Theorems · Theorem · order theory
Set.compl_empty
∀ {α : Type u_1}, ∅ᶜ = Set.univ- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 33 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 · cited by 53,352
- Set.univstatement · cited by 3,945
- Compl.complstatement · cited by 2,925
- compl_botproof · cited by 8
Cited by33
Results whose statement or proof uses this declaration.
- PrimeSpectrum.basicOpen_oneproof · cited by 7
- Bornology.isBounded_emptyproof · cited by 5
- MeasureTheory.ae_eq_botproof · cited by 4
- Affine.Simplex.ExcenterExists.touchpoint_injectiveproof · cited by 4
- preconnectedSpace_iff_clopenproof · cited by 3
- SSet.nondegenerate_zeroproof · cited by 3
- MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRTproof · cited by 2
- Filter.totallyBounded_iff_filterproof · cited by 2
- Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mulproof · cited by 2
- MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_ltproof · cited by 2
- Measurable.isLUB_of_memproof · cited by 2
- le_cofinite_iff_boundaryproof · cited by 1