mk_le_one_iff_set_subsingleton — Mathlib

English

Let s be a subset of α. Then |s| ≤ 1 if and only if s has at most one element (i.e., s is subsingleton).

Русский

Пусть s⊆α. Тогда |s| ≤ 1 тогда и только тогда множество s содержит не более одного элемента (то есть является subsingleton).

LaTeX

$$$|s| \le 1 \iff \forall x \in s \forall y \in s\, (x = y)$$$

Lean4

@[simp]
theorem mk_le_one_iff_set_subsingleton {s : Set α} : #s ≤ 1 ↔ s.Subsingleton :=
  le_one_iff_subsingleton.trans s.subsingleton_coe

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