div_eq_one_iff — Mathlib

English

Let a,b ∈ ENNReal with hb0: b ≠ 0 and hb1: b ≠ ∞. Then a/b = 1 if and only if a = b.

Русский

Пусть a,b ∈ ENNReal и b ≠ 0, b ≠ ∞. Тогда a/b = 1 тогда и только тогда, когда a = b.

LaTeX

$$$$\forall a,b \in \mathbb{R}_{\ge 0}^{\infty},\ b \neq 0 \land b \neq \infty \Rightarrow \frac{a}{b} = 1 \iff a = b.$$$$

Lean4

theorem div_eq_one_iff {a b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb₁ : b ≠ ∞) : a / b = 1 ↔ a = b :=
  ⟨fun h => by rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one], fun h => h.symm ▸ ENNReal.div_self hb₀ hb₁⟩

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