infinite_of_forall_exists_gt — Mathlib

English

If for every a there exists b ∈ s with a < b in a preorder, then s is infinite.

Русский

Если для каждого a существует b ∈ s, такой что a < b, в предордере, то s бесконечно.

LaTeX

$$$\forall a\,\exists b\ (b \in s \wedge a < b) \Rightarrow s \text{ is infinite}.$$$

Lean4

theorem infinite_of_forall_exists_gt (h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite :=
  by
  inhabit α
  let f (n : ℕ) : α := Nat.recOn n (h default).choose fun _ a ↦ (h a).choose
  have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
  exact infinite_of_injective_forall_mem (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

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