one_lt_card_iff

Mathlib.Data.Fintype.EquivFin

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

English

1 < card α iff there exist two distinct elements.

Русский

1 < card α эквивалентно существованию двух различных элементов.

LaTeX

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

Lean4

theorem one_lt_card_iff : 1 < card α ↔ ∃ a b : α, a ≠ b :=
  one_lt_card_iff_nontrivial.trans nontrivial_iff

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

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

Разделы

Аффилиация

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