eq_top_iff_forall_lt — Mathlib

English

An element x equals the top if and only if every real y embedded in EReal is less than x.

Русский

Элемент x равен верхнему, если и только если каждый вещественный y, вложенный в EReal, меньше x.

LaTeX

$$$x = \top \iff \forall y \in \mathbb{R}, (y:EReal) < x$$$

Lean4

theorem eq_top_iff_forall_lt (x : EReal) : x = ⊤ ↔ ∀ y : ℝ, (y : EReal) < x :=
  by
  constructor
  · rintro rfl
    exact EReal.coe_lt_top
  · contrapose!
    intro h
    exact ⟨x.toReal, le_coe_toReal h⟩

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