Revision #1289 → #2955 · back to history
addedEx falso: contradiction implies anything4fc237bf0719
addedNegated elements form a Boolean lattice01e424b0760d
modifiedComplemented elements485f6b59c3a1
| Field | From #1289 | To #2955 |
|---|
| mathlib.module | Mathlib.Order.BooleanAlgebra.Defs | Mathlib.Order.Disjoint |
| note | `IsCompl a b` (defined in `Mathlib.Order.Disjoint`) captures complementarity by `Disjoint` and `Codisjoint`. | `IsCompl a b` captures complementarity via `Disjoint` and `Codisjoint`. |
modifiedHeyting algebras form a category4c4ab9ed444b
| Field | From #1289 | To #2955 |
|---|
| mathlib.decl | — | HeytAlg |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Order.Category.HeytAlg |
| note | No bundled `HeytAlg` category of Heyting algebras is defined in Mathlib. | `HeytAlg` bundles the category of Heyting algebras with `HeytingHom` morphisms. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |