Documentation

PFR.Mathlib.Data.Set.Basic

@[simp]
theorem Set.inter_eq_left' {α : Type u} {s t : Set α} :
s ts t = s

Alias of the reverse direction of Set.inter_eq_left.

@[simp]
theorem Set.inter_eq_right' {α : Type u} {s t : Set α} :
t ss t = t

Alias of the reverse direction of Set.inter_eq_right.