Mathlib Map

Theorems · Inductive type · order theory

Order.Coframe

Type u_1 → Type u_1

A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice whose ⊔ distributes over ⨅.

Defined in
Mathlib.Order.CompleteBooleanAlgebra
Cited by
38 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

iInf_sup_eq · cited by 7iInf_sup_eqsup_iInf_eq · cited by 6sup_iInf_eqsup_sInf_eq · cited by 4sup_sInf_eqsInf_sup_eq · cited by 3sInf_sup_eqiInf_iSup_of_monotone · cited by 3iInf_iSup_of_monotoneiInf_sup_iInf · cited by 3iInf_sup_iInfiInf_sup_of_monotone · cited by 3iInf_sup_of_monotonebiInf_sup_biInf · cited by 2biInf_sup_biInfiInf_codisjoint_iff · cited by 2iInf_codisjoint_iffiInf_iSup_of_antitone · cited by 2iInf_iSup_of_antitoneSet.Finite.iInf_biSup_of_monotone · cited by 2Finite.iInf_biSup_of_mono…Order.Coframe.toSDiff · cited by 2Coframe.toSDiffsInf_sup_sInf · cited by 1sInf_sup_sInfIsCoatom.iInf_le · cited by 1IsCoatom.iInf_lecodisjoint_iInf_iff · cited by 1codisjoint_iInf_iffOrder.CoframeCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by53

Results whose statement or proof uses this declaration.