Theorems · Theorem · logic and foundations
Set.notMem_subset
∀ {α : Type u} {a : α} {s t : Set α}, s ⊆ t → a ∉ t → a ∉ s- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
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.mem_of_subset_of_memproof · cited by 48
Cited by18
Results whose statement or proof uses this declaration.
- Matroid.Indep.exists_insert_of_not_isBaseproof · cited by 5
- AffineIndependent.eq_zero_of_affineCombination_mem_affineSpanproof · cited by 4
- OnePoint.infty_notMem_image_coeproof · cited by 4
- Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subsetproof · cited by 3
- SummationFilter.eventually_mem_or_not_memproof · cited by 2
- totallySeparatedSpace_of_t0_of_basis_clopenproof · cited by 2
- Matroid.exists_isCircuit_of_mem_closureproof · cited by 2
- exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhdsproof · cited by 1
- SimpleGraph.ComponentCompl.hom_mkstatement · cited by 1
- Matroid.Indep.union_indep_iff_forall_notMem_closure_rightproof · cited by 1
- PMF.toOuterMeasure_apply_eq_one_iffproof · cited by 1
- MeasureTheory.lintegral_iSup_aeproof · cited by 1