Theorems · Theorem · order theory
Set.subset_compl_comm
∀ {α : Type u_1} {s t : Set α}, s ⊆ tᶜ ↔ t ⊆ sᶜ- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 22 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.
Cites3
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
- le_compl_iff_le_complproof · cited by 3
Cited by22
Results whose statement or proof uses this declaration.
- Set.subset_sdiff_singletonproof · cited by 14
- MeasureTheory.Measure.dirac_applyproof · cited by 9
- Set.subset_compl_singleton_iffproof · cited by 7
- regularSpace_TFAEproof · cited by 6
- isCompact_of_finite_subcoverproof · cited by 5
- exists_continuous_one_zero_of_isCompactproof · cited by 5
- Algebra.basicOpen_subset_etaleLocus_iffproof · cited by 3
- Algebra.basicOpen_subset_smoothLocus_iffproof · cited by 3
- Algebra.basicOpen_subset_unramifiedLocus_iffproof · cited by 3
- precise_refinement_setproof · cited by 3
- PeriodPair.hasFPowerSeriesOnBall_weierstrassPExceptproof · cited by 3
- Ideal.disjoint_primeCompl_of_liesOverproof · cited by 3