eq_bot_iff_forall_lt — Mathlib

English

An element x equals the bottom if and only if every real y satisfies x < y embedded in EReal.

Русский

Элемент x равен нижнему, если и только если для каждого вещественного y верно x < y (в EReal).

LaTeX

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

Lean4

theorem eq_bot_iff_forall_lt (x : EReal) : x = ⊥ ↔ ∀ y : ℝ, x < (y : EReal) :=
  by
  constructor
  · rintro rfl
    exact bot_lt_coe
  · contrapose!
    intro h
    exact ⟨x.toReal, coe_toReal_le h⟩

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