Theorems · Theorem · order theory
Set.sdiff_eq_empty
∀ {α : Type u_1} {s t : Set α}, s \ t = ∅ ↔ s ⊆ t- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 24 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.
Cites2
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
- sdiff_eq_bot_iffproof · cited by 10
Cited by24
Results whose statement or proof uses this declaration.
- MeasureTheory.SimpleFunc.inductionproof · cited by 14
- isClopen_iff_frontier_eq_emptyproof · cited by 6
- Matroid.closure_union_eq_of_subset_coloopsproof · cited by 4
- Set.Finite.eq_of_subset_of_encard_le'proof · cited by 4
- Set.sdiff_nonempty_of_ncard_lt_ncardproof · cited by 3
- MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_topproof · cited by 3
- Set.sdiff_univproof · cited by 3
- Matroid.IsBase.exchange_isBase_of_indepproof · cited by 3
- Subalgebra.spectrum_sUnion_connectedComponentInproof · cited by 2
- dense_compl_of_dimH_lt_finrankproof · cited by 2
- self_sdiff_frontierproof · cited by 2
- Set.Finite.ecard_lt_ecardproof · cited by 2