exists_pair_of_one_lt_card

Mathlib.Data.Fintype.EquivFin

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

English

If card α > 1, there exist a,b ∈ α with a ≠ b.

Русский

Если в α больше одного элемента, то существуют элементы a,b ∈ α такие, что a ≠ b.

LaTeX

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

Lean4

theorem exists_pair_of_one_lt_card (h : 1 < card α) : ∃ a b : α, a ≠ b :=
  haveI : Nontrivial α := one_lt_card_iff_nontrivial.1 h
  exists_pair_ne α

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

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

Разделы

Аффилиация

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