Theorems · Theorem · group theory
Set.add_subset_add
∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂- Cited by
- 18 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- Add
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
- Set.addstatement · cited by 338
- Set.image2_subsetproof · cited by 25
Cited by18
Results whose statement or proof uses this declaration.
- Convex.combo_interior_closure_subset_interiorproof · cited by 3
- Balanced.addproof · cited by 3
- exists_closed_nhds_zero_neg_eq_add_subsetproof · cited by 3
- Absorbs.addproof · cited by 3
- StrictConvex.addproof · cited by 2
- convexHull_add_subsetproof · cited by 1
- Set.list_sum_subset_list_sumproof · cited by 1
- MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translatesproof · cited by 1
- Convex.combo_interior_self_subset_interiorproof · cited by 1
- MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_oneproof · cited by 1
- MeasureTheory.hasFDerivAt_convolution_right_with_paramproof · cited by 1
- HasCompactSupport.convolutionproof · cited by 0