Theorems · Theorem · order theory
Set.union_singleton
∀ {α : Type u_1} {s : Set α} {a : α}, s ∪ {a} = insert a s- Defined in
- Mathlib.Data.Set.Insert
- Cited by
- 107 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 25 definitions · uses propext, 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
- Set.union_commproof · cited by 99
Cited by107
Results whose statement or proof uses this declaration.
- Set.encard_insert_of_notMemproof · cited by 17
- fg_adjoin_of_finiteproof · cited by 9
- SSet.horn_eq_iSupproof · cited by 9
- Real.continuous_mul_logproof · cited by 9
- MeasureTheory.integral_trimproof · cited by 6
- Ideal.height_le_spanRank_toENat_of_mem_minimalPrimesproof · cited by 5
- FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentenceproof · cited by 5
- MeasureTheory.SimpleFunc.memLp_approxOn_rangeproof · cited by 4
- Set.injOn_insertproof · cited by 4
- Cardinal.mk_insertproof · cited by 3
- CFC.monotone_nnrpowproof · cited by 3
- finite_memPartitionproof · cited by 3