infinite_iff_exists_gt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Set.infinite_iff_exists_gt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, a < b :=
  ⟨Set.Infinite.exists_gt, Set.infinite_of_forall_exists_gt⟩

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