le_of_top_imp_top_of_toNNReal_le — Mathlib

English

Let a,b ∈ ENNReal. If a = ∞ → b = ∞ and a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal, then a ≤ b.

Русский

Пусть a,b ∈ ENNReal. Если a = ∞ → b = ∞ и a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal, тогда a ≤ b.

LaTeX

$$$$\\bigl(a = \\infty \\rightarrow b = \\infty\\bigr) \\wedge \\bigl(a \\neq \\infty \\rightarrow b \\neq \\infty \\rightarrow a^{\\nnReal} \\le b^{\\nnReal}\\bigr) \\Rightarrow a \\le b$$$$

Lean4

theorem le_of_top_imp_top_of_toNNReal_le {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤)
    (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b :=
  by
  by_contra! hlt
  lift b to ℝ≥0 using hlt.ne_top
  lift a to ℝ≥0 using mt h coe_ne_top
  refine hlt.not_ge ?_
  simpa using h_nnreal

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