LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Insert

Imported Lean Pool material for LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Insert.

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

Alias of the reverse direction of Set.inter_singleton_eq_empty.

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

Alias of the reverse direction of Set.singleton_inter_eq_empty.