one_lt_card

Mathlib.Data.Fintype.EquivFin

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

English

1 < card α if and only if there exist a,b ∈ α with a ≠ b.

Русский

1 < card α тогда и только тогда, когда существуют a,b ∈ α такие, что a ≠ b.

LaTeX

$$$1 < \\operatorname{card} \\alpha \\iff \\exists a,b: \\alpha, a \\neq b$$$

Lean4

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

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

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

Разделы

Аффилиация

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