not_infinite_iff_exist_lt_gt — Mathlib

English

A hyperreal x is finite iff there exist real numbers r and s with r < x < s.

Русский

Гиперреальное x конечно тогда и только тогда, когда существуют вещественные r и s такие, что r < x < s.

LaTeX

$$$\\neg Infinite(x) \\iff \\exists r,s \\in \\mathbb{R}, (r : \\mathbb{R}^*) < x \\land x < s$$$

Lean4

theorem not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬Infinite x ↔ ∃ r s : ℝ, (r : ℝ*) < x ∧ x < s :=
  ⟨fun hni ↦
    let ⟨r, hr⟩ := exists_st_of_not_infinite hni;
    ⟨r - 1, r + 1, hr 1 one_pos⟩,
    fun ⟨r, s, hr, hs⟩ hi ↦ hi.elim (fun hp ↦ (hp s).not_gt hs) (fun hn ↦ (hn r).not_gt hr)⟩

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