inv_lt_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inv_lt_top (x : EReal) : x⁻¹ < ⊤ := by
  cases x with
  | bot => exact inv_bot ▸ zero_lt_top
  | top => exact EReal.inv_top ▸ zero_lt_top
  | coe x => exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

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