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

@[simp]

theorem Set.ne_empty_iff_nonempty {α : Type u_1} {s : Set α} : s ≠ ∅ ↔ s.Nonempty