exists_between_coe_real — Mathlib

English

If x < z in EReal, there exists a real y with x < y < z.

Русский

Если x < z в EReal, существует вещественное y такое, что x < y < z.

LaTeX

$$$x < z \Rightarrow \exists y \in \mathbb{R}, x < y \land y < z$$$

Lean4

theorem exists_between_coe_real {x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z :=
  by
  obtain ⟨a, ha₁, ha₂⟩ := exists_between h
  induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim

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