@[simp]

theorem Set.inter_singleton_eq_empty' {α : Type u} {s : Set α} {a : α} : ¬a ∈ s → s ∩ {a} = ∅

Alias of the reverse direction of Set.inter_singleton_eq_empty.

@[simp]

theorem Set.singleton_inter_eq_empty' {α : Type u} {s : Set α} {a : α} : ¬a ∈ s → {a} ∩ s = ∅

Alias of the reverse direction of Set.singleton_inter_eq_empty.