toReal_pos_iff_ne_top — Mathlib

English

Let p be an extended nonnegative real with p ≥ 1. Then p.toReal is positive if and only if p is not the top element ∞.

Русский

Пусть p ∈ ℝ≥0∞ с p ≥ 1. Тогда p.toReal > 0 тогда и только тогда, когда p ≠ ∞.

LaTeX

$$$$0 < \\operatorname{toReal}(p) \\iff p \\neq \\infty\\quad\\text{for } p \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; 1 \\le p.$$$$

Lean4

theorem toReal_pos_iff_ne_top (p : ℝ≥0∞) [Fact (1 ≤ p)] : 0 < p.toReal ↔ p ≠ ∞ :=
  ⟨fun h hp =>
    have : (0 : ℝ) ≠ 0 := toReal_top ▸ (hp ▸ h.ne : 0 ≠ ∞.toReal)
    this rfl,
    fun h => zero_lt_one.trans_le (p.dichotomy.resolve_left h)⟩

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