Theorems · Theorem · order theory
Set.subset_insert
∀ {α : Type u_1} (x : α) (s : Set α), s ⊆ insert x s- Defined in
- Mathlib.Data.Set.Insert
- Cited by
- 96 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 17 definitions · 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 by96
Results whose statement or proof uses this declaration.
- Ideal.IsMaximal.isPrimeproof · cited by 53
- ContDiffWithinAt.differentiableWithinAtproof · cited by 19
- Matroid.IsBasis.closure_eq_closureproof · cited by 13
- ContDiffWithinAt.analyticWithinAtproof · cited by 13
- Submodule.span_insert_zeroproof · cited by 11
- nhdsWithin_insert_of_neproof · cited by 9
- ContDiffWithinAt.eventuallyproof · cited by 9
- Matroid.Indep.closure_eq_setOfPred_isBasis_insertproof · cited by 6
- Submodule.span_insert_eq_spanproof · cited by 5
- Maximal.mem_of_prop_insertproof · cited by 5
- contDiffWithinAt_succ_iff_hasFDerivWithinAtproof · cited by 5
- Ideal.IsMaximal.exists_invproof · cited by 4