Theorems · Theorem · logic and foundations
Set.mem_union_left
∀ {α : Type u} {x : α} {a : Set α} (b : Set α), x ∈ a → x ∈ a ∪ b- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by32
Results whose statement or proof uses this declaration.
- Polynomial.Splits.Cproof · cited by 9
- eVariationOn.unionproof · cited by 4
- GromovHausdorff.ghDist_le_hausdorffDistproof · cited by 3
- StarAlgebra.self_mem_adjoin_singletonproof · cited by 3
- AffineSubspace.direction_supproof · cited by 2
- rieszContentAux_unionproof · cited by 2
- SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_interproof · cited by 2
- MeasurableSpace.compl_mem_generateMeasurableRecproof · cited by 2
- MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subsetproof · cited by 2
- linearIndependent_set_iff_affineIndependent_vadd_union_singletonproof · cited by 2
- MeasurableSpace.empty_mem_generateMeasurableRecproof · cited by 2
- Algebra.FinitePresentation.of_restrict_scalars_finitePresentationproof · cited by 2