Theorems · Theorem · order theory
Set.singleton_union
∀ {α : Type u_1} {s : Set α} {a : α}, {a} ∪ s = insert a s- Defined in
- Mathlib.Data.Set.Insert
- Cited by
- 22 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 by22
Results whose statement or proof uses this declaration.
- nhdsWithin_insertproof · cited by 13
- IsRelPrime.isCoprimeproof · cited by 5
- alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_fourproof · cited by 4
- RingHom.IsIntegralElem.of_mem_closureproof · cited by 4
- Matroid.closure_union_eq_of_subset_coloopsproof · cited by 4
- Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulproof · cited by 3
- Matroid.IsBasis.contract_eq_contract_deleteproof · cited by 3
- Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subsetproof · cited by 3
- IntermediateField.finiteDimensional_adjoin_pairproof · cited by 2
- Matroid.IsNonloop.mem_closure_singletonproof · cited by 2
- measure_eq_measure_preimage_add_measure_tsum_Ico_zpowproof · cited by 2
- Matrix.range_cons_cons_emptyproof · cited by 2