Mathlib Map

Theorems · Theorem · order theory

Set.notMem_sdiff_of_mem

∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ t → x ∉ s \ t
Defined in
Mathlib.Order.BooleanAlgebra.Set
Cited by
7 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

nhdsWithin_insert_of_ne · cited by 9nhdsWithin_insert_of_neTopologicalSpace.exists_countable_basis · cited by 9TopologicalSpace.exists_c…closure_sUnion_irreducibleComponents_sdiff_singleton · cited by 2closure_sUnion_irreducibl…finprod_mem_powerset_sdiff_elem · cited by 1finprod_mem_powerset_sdif…Set.Finite.encard_biUnion · cited by 1Finite.encard_biUnionfinsum_mem_powerset_sdiff_elem · cited by 0finsum_mem_powerset_sdiff…Set.notMem_diff_of_mem · cited by 0Set.notMem_diff_of_memSet · cited by 53352SetSet.notMem_sdiff_of_memCITED 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 by7

Results whose statement or proof uses this declaration.