Theorems · Theorem · order theory
Set.sdiff_subset_sdiff
∀ {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 11 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_le_sdiffproof · cited by 16
Cited by11
Results whose statement or proof uses this declaration.
- Continuous.frontier_preimage_subsetproof · cited by 2
- setOfPred_liouville_eq_irrational_inter_iInter_iUnionproof · cited by 2
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closedproof · cited by 2
- frontier_interior_subsetproof · cited by 1
- closure_sdiffproof · cited by 1
- Matroid.IsCircuit.strong_eliminationproof · cited by 1
- MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zeroproof · cited by 1
- Besicovitch.exist_finset_disjoint_balls_large_measureproof · cited by 1
- Set.diff_subset_diffproof · cited by 0
- Matroid.IsCircuit.strong_multi_elimination_setproof · cited by 0
- frontier_closure_subsetproof · cited by 0