Def Order.Frame.MinimalAxioms.of

Modification history

2025-02-05 05:32

Mathlib/Order/CompleteBooleanAlgebra.lean

refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391) …

Modified Order.Frame.MinimalAxioms.of View on Github →

2024-07-23 12:07

Mathlib/Order/CompleteBooleanAlgebra.lean

refactor: Make `Frame` extend `HeytingAlgebra` (#10560) …

Added Order.Frame.MinimalAxioms.of View on Github →