not_nontrivial

Mathlib.Logic.Nontrivial.Defs

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

English

If α is subsingleton, then α is not nontrivial.

Русский

Если α является subsingleton, то она не не тривиальна.

LaTeX

$$$(\text{Subsingleton}(\alpha)) \Rightarrow \neg\text{Nontrivial}(\alpha)$$$

Lean4

theorem not_nontrivial (α) [Subsingleton α] : ¬Nontrivial α := fun ⟨⟨x, y, h⟩⟩ ↦ h <| Subsingleton.elim x y

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

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

Разделы

Аффилиация

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