one_lt_card

Mathlib.Data.Finite.Card

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

English

If α is finite and nontrivial, then 1 < Nat.card α.

Русский

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

LaTeX

$$$[Finite\alpha]\ [Nontrivial(\alpha)] \Rightarrow 1 < Nat.card(\alpha)$$$

Lean4

theorem one_lt_card [Finite α] [h : Nontrivial α] : 1 < Nat.card α :=
  one_lt_card_iff_nontrivial.mpr h

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

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

Разделы

Аффилиация

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