not_subsingleton

Mathlib.Logic.Nontrivial.Defs

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

English

If α is nontrivial, then α is not subsingleton.

Русский

Если α не тривиален, тогда он не subsingleton.

LaTeX

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

Lean4

theorem not_subsingleton (α) [Nontrivial α] : ¬Subsingleton α := fun _ => not_nontrivial _ ‹_›

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

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

Разделы

Аффилиация

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