one_lt_card

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#ENat.one_lt_card

English

If α is nontrivial, then 1 < card α.

Русский

Если α не тривиален, то 1 < card α.

LaTeX

$$$$ \\text{Nontrivial}(\\alpha) \\Rightarrow 1 < \\operatorname{card} \\alpha. $$$$

Lean4

@[simp]
theorem one_lt_card [Nontrivial α] : 1 < card α := by simpa [one_lt_card_iff_nontrivial]

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

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

Разделы

Аффилиация

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