Theorems · Theorem · order theory
Set.sdiff_subset_sdiff_right
∀ {α : Type u_1} {s t u : Set α}, t ⊆ u → s \ u ⊆ s \ t- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 12 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
- le_reflproof · cited by 2,061
- sdiff_le_sdiffproof · cited by 16
Cited by12
Results whose statement or proof uses this declaration.
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_setproof · cited by 3
- MeasureTheory.Content.borel_le_caratheodoryproof · cited by 1
- Directed.measure_iInterproof · cited by 1
- MeasureTheory.SignedMeasure.exists_subset_restrict_nonposproof · cited by 1
- IsCountablyCompact.elim_directed_coverproof · cited by 1
- Matroid.Indep.contract_isBase_iffproof · cited by 1
- MeasureTheory.tendsto_setIntegral_of_antitoneproof · cited by 1
- Matroid.IsBasis.contract_sdiff_isBasis_sdiffproof · cited by 1
- Set.diff_subset_diff_rightproof · cited by 0
- SimpleGraph.Subgraph.deleteVerts_antiproof · cited by 0