Theorems · Theorem · order theory
Set.subset_compl_iff_disjoint_left
∀ {α : Type u_1} {s t : Set α}, s ⊆ tᶜ ↔ Disjoint t s- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Compl.complstatement · cited by 2,925
- Disjointstatement · cited by 2,201
- le_compl_iff_disjoint_leftproof · cited by 7
Cited by9
Results whose statement or proof uses this declaration.
- Disjoint.subset_compl_leftproof · cited by 13
- MeasureTheory.hahn_decompositionproof · cited by 2
- disjoint_principal_nhdsSetproof · cited by 2
- ContinuousMap.idealOfSet_ofIdeal_eq_closureproof · cited by 2
- Filter.disjoint_principal_principalproof · cited by 1
- exists_contMDiffMap_zero_one_nhds_of_isClosedproof · cited by 1
- Topology.IsInducing.completelyNormalSpaceproof · cited by 1
- exists_contMDiffMap_one_nhds_of_subset_interiorproof · cited by 0
- AlgebraicGeometry.isClosedImmersion_of_comp_eq_idproof · cited by 0