dichotomy — Mathlib

English

For any p ∈ ENNReal with a Fact that 1 ≤ p, we have p = ∞ or 1 ≤ p.toReal.

Русский

Для любого p ∈ ENNReal с условием 1 ≤ p имеем либо p = ∞, либо 1 ≤ p.toReal.

LaTeX

$$∀ p ∈ ENNReal, [Fact (1 ≤ p)] → p = ∞ ∨ 1 ≤ p.toReal$$

Lean4

protected theorem dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal :=
  haveI : p = ⊤ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal := by simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)
  this.imp_right fun h => h.2

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