bot_lt_inv — Mathlib

English

For every x ∈ EReal, the bottom element is strictly less than its inverse: ⊥ < x^{-1}.

Русский

Для любого x ∈ EReal нижняя граница строго меньше своего обратного: ⊥ < x^{-1}.

LaTeX

$$$ \bot < x^{-1} $$$

Lean4

theorem bot_lt_inv (x : EReal) : ⊥ < x⁻¹ := by
  cases x with
  | bot => exact inv_bot ▸ bot_lt_zero
  | top => exact EReal.inv_top ▸ bot_lt_zero
  | coe x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

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