subsingleton_iff

Mathlib.Logic.Nontrivial.Defs

URI: https://scilib.ai/kg/mathlib#subsingleton_iff

English

Subsingleton α is equivalent to ∀ x,y, x = y.

Русский

Subsingleton α эквивалентно тому, что для любых x,y верно x = y.

LaTeX

$$$\text{Subsingleton}(\alpha) \iff \forall x,y:\, \alpha, x = y$$$

Lean4

theorem subsingleton_iff : Subsingleton α ↔ ∀ x y : α, x = y :=
  ⟨by
    intro h
    exact Subsingleton.elim, fun h ↦ ⟨h⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru