Theorems · Theorem · order theory
Set.compl_subset_comm
∀ {α : Type u_1} {s t : Set α}, sᶜ ⊆ t ↔ tᶜ ⊆ s- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 23 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
- compl_le_iff_compl_leproof · cited by 2
Cited by23
Results whose statement or proof uses this declaration.
- MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eqproof · cited by 9
- spectrum.zero_eqproof · cited by 7
- Filter.mem_cocompact'proof · cited by 5
- normal_exists_closure_subsetproof · cited by 5
- isInducing_stoneCechUnitproof · cited by 4
- Filter.mem_coclosedCompact_iffproof · cited by 3
- Filter.hasBasis_cofiniteproof · cited by 3
- exists_tsupport_one_of_isOpen_isClosedproof · cited by 2
- HasCompactSupport.is_zero_at_inftyproof · cited by 2
- FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realizeproof · cited by 2
- PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopenproof · cited by 2
- mem_fixingAddSubgroup_compl_iff_movedBy_subsetproof · cited by 1