Theorems · Theorem · order theory
disjoint_compl_left
∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, Disjoint aᶜ a- Defined in
- Mathlib.Order.Heyting.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- HeytingAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Compl.complstatement · cited by 2,925
- Disjointstatement · cited by 2,201
- Eq.geproof · cited by 375
- HeytingAlgebrastatement and proof · cited by 108
- disjoint_iff_inf_leproof · cited by 64
- le_himp_iffproof · cited by 19
- himp_botproof · cited by 9
Cited by17
Results whose statement or proof uses this declaration.
- disjoint_compl_rightproof · cited by 47
- IsCompl.compl_eqproof · cited by 16
- regularSpace_TFAEproof · cited by 6
- Disjoint.closure_leftproof · cited by 6
- IsLocalization.AtPrime.isUnit_to_map_iffproof · cited by 4
- IsCompl.eq_complproof · cited by 4
- isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_leproof · cited by 2
- compl_bihimp_selfproof · cited by 2
- LE.le.disjoint_compl_leftproof · cited by 2
- totallySeparatedSpace_of_t0_of_basis_clopenproof · cited by 2
- MeasurableSpace.DynkinSystem.has_sdiffproof · cited by 1
- disjoint_nhds_atTop_iffproof · cited by 1