Theorems · Theorem · order theory
IsCompl.compl_eq
∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → aᶜ = b- Defined in
- Mathlib.Order.Heyting.Basic
- Cited by
- 16 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Compl.complstatement · cited by 2,925
- IsComplstatement and proof · cited by 351
- HeytingAlgebrastatement and proof · cited by 108
- LE.le.antisymm'proof · cited by 104
- IsCompl.disjointproof · cited by 42
- IsCompl.codisjointproof · cited by 32
- disjoint_compl_leftproof · cited by 17
- Disjoint.le_compl_leftproof · cited by 3
- Disjoint.le_of_codisjointproof · cited by 3
Cited by16
Results whose statement or proof uses this declaration.
- compl_complproof · cited by 229
- HasSum.add_isComplproof · cited by 4
- HasProd.mul_isComplproof · cited by 4
- Set.compl_range_inrproof · cited by 3
- compl_eq_iff_isComplproof · cited by 2
- Set.compl_range_someproof · cited by 2
- IsCompl.compl_eq_iffproof · cited by 2
- Order.Ideal.PrimePair.compl_I_eq_Fproof · cited by 2
- OnePoint.compl_inftyproof · cited by 1
- compl_uniqueproof · cited by 1
- Set.compl_range_inlproof · cited by 1
- SimpleGraph.IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraphproof · cited by 1