eq_of_nonempty_of_subsingleton — Mathlib

English

If α is a Subsingleton and s,t are subsets of α with Nonempty elements, then s = t.

Русский

Если α — субодиночка, и s,t — подмножества α с непустыми элементами, тогда s = t.

LaTeX

$$$\text{Let } \alpha \text{ be a Subsingleton. If } s,t \subseteq \alpha \text{ with } s, t \neq \emptyset, \text{ then } s = t.$$$

Lean4

theorem eq_of_nonempty_of_subsingleton {α} [Subsingleton α] (s t : Set α) [Nonempty s] [Nonempty t] : s = t :=
  Nonempty.of_subtype.eq_univ.trans Nonempty.of_subtype.eq_univ.symm

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