le_of_forall_lt_iff_le — Mathlib

English

Let x,y ∈ EReal. Then the following are equivalent: (∀ z ∈ ℝ, x < z → y ≤ z) and (y ≤ x).

Русский

Пусть x,y ∈ EReal. Тогда эквивалентны условия: (∀ z ∈ ℝ, x < z → y ≤ z) и (y ≤ x).

LaTeX

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

Lean4

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

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