eq_of_nonempty_of_subsingleton' — Mathlib

English

In a Subsingleton type, given any two nonempty sets s,t, s = t.

Русский

В типе с-subsingleton, любые две непустые подмножества совпадают.

LaTeX

$$$\text{In a Subsingleton } \alpha, \text{ for any } s,t \subseteq \alpha, \text{ if } s \neq \emptyset, t \neq \emptyset, \; s = t.$$$

Lean4

theorem eq_of_nonempty_of_subsingleton' {α} [Subsingleton α] {s : Set α} (t : Set α) (hs : s.Nonempty) [Nonempty t] :
    s = t :=
  have := hs.to_subtype;
  eq_of_nonempty_of_subsingleton s t

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