Mathlib Map

Theorems · Theorem · order theory

Set.ssubset_insert

∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s ⊂ insert a s
Defined in
Mathlib.Data.Set.Insert
Cited by
6 results in Mathlib
Foundations
Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matroid.IsBasis.insert_dep · cited by 3IsBasis.insert_depSet.covBy_insert · cited by 2Set.covBy_insertSet.Finite.induction_to · cited by 1Finite.induction_toCovBy.exists_set_insert · cited by 1CovBy.exists_set_insertMatroid.IsBase.dep_of_insert · cited by 1IsBase.dep_of_insertMatroid.IsBase.insert_not_isBase · cited by 0IsBase.insert_not_isBaseSet · cited by 53352SetSet.ssubset_insertCITED BYCITES

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 by6

Results whose statement or proof uses this declaration.