one_lt_card — Mathlib

English

A finite set has size greater than one iff there exist two distinct elements in the set.

Русский

Конечное множество имеет размер больше единицы тогда и только тогда, когда в нём есть два разных элемента.

LaTeX

$$1 < #s ↔ ∃ a ∈ s ∃ b ∈ s, a ≠ b$$

Lean4

theorem one_lt_card : 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b :=
  by
  rw [← not_iff_not]
  push_neg
  exact card_le_one

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