mem_diff_singleton_empty — Mathlib

English

For a family t of subsets of α, s ∈ t \ {∅} iff s ∈ t and s is nonempty.

Русский

Для семейства t подмножеств α: s ∈ t \ {∅} тогда и только тогда, когда s ∈ t и s не пусто.

LaTeX

$$$$ s \in t \setminus \{\emptyset\} \iff (s \in t) \land (s \neq \emptyset). $$$$

Lean4

theorem mem_diff_singleton_empty {t : Set (Set α)} : s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty :=
  mem_diff_singleton.trans <| and_congr_right' nonempty_iff_ne_empty.symm

Похожие утверждения