Theorems · Theorem · order theory
IsCompl.eq_compl
∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → a = bᶜ- Defined in
- Mathlib.Order.Heyting.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext
- Assumes
- HeytingAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Compl.complstatement · cited by 2,925
- LE.le.antisymmproof · cited by 507
- IsComplstatement and proof · cited by 351
- HeytingAlgebrastatement and proof · cited by 108
- IsCompl.disjointproof · cited by 42
- IsCompl.codisjointproof · cited by 32
- disjoint_compl_leftproof · cited by 17
- Codisjoint.symmproof · cited by 9
- Disjoint.le_compl_rightproof · cited by 3
- Disjoint.le_of_codisjointproof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- eq_compl_iff_isComplproof · cited by 6
- MeasurableSpace.measurableSet_generateFrom_memPartition_iffproof · cited by 1
- Order.Ideal.PrimePair.compl_F_eq_Iproof · cited by 1
- IsCompl.bihimp_eq_botproof · cited by 0