infinite_iff_exists_lt — Mathlib

English

For a set s, s is infinite iff for every a there exists b ∈ s with b < a.

Русский

Для множества s бесконечно тогда и только тогда, когда для каждого a существует b ∈ s с b < a.

LaTeX

$$|s| = \infty \iff (\forall a, \exists b \in s, b < a)$$

Lean4

theorem _root_.Set.infinite_iff_exists_lt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, b < a :=
  ⟨Set.Infinite.exists_lt, Set.infinite_of_forall_exists_lt⟩

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