ge_of_forall_gt_iff_ge — Mathlib

English

Let x,y ∈ EReal. Then (∀ z ∈ ℝ, z < y → z ≤ x) ↔ y ≤ x.

Русский

Пусть x,y ∈ EReal. Тогда (∀ z ∈ ℝ, z < y → z ≤ x) ↔ y ≤ x.

LaTeX

$$$\forall x,y \in \mathrm{EReal},\ (\forall z \in \mathbb{R},\ z < y \rightarrow z \le x) \iff y \le x$$$

Lean4

theorem ge_of_forall_gt_iff_ge {x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x :=
  by
  refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
  rw [WithTop.forall]
  aesop

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