@[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.