LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Basic

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

@[simp]

theorem Set.inter_eq_left' {α : Type u} {s t : Set α} : s ⊆ t → s ∩ t = s

Alias of the reverse direction of Set.inter_eq_left.

@[simp]

theorem Set.inter_eq_right' {α : Type u} {s t : Set α} : t ⊆ s → s ∩ t = t

Alias of the reverse direction of Set.inter_eq_right.