isSt_inj_real — Mathlib

English

If two real numbers r1 and r2 are both IsSt to the same s, then r1 = r2.

Русский

Если r1 и r2 два вещественных числа, и IsSt r1 s, IsSt r2 s, то r1 = r2.

LaTeX

$$$\forall r_1,r_2,s\in \mathbb{R}, \ (\mathrm{IsSt}(r_1,s) \rightarrow \mathrm{IsSt}(r_2,s) \rightarrow r_1 = r_2)$$$

Lean4

theorem isSt_inj_real {r₁ r₂ s : ℝ} (h1 : IsSt r₁ s) (h2 : IsSt r₂ s) : r₁ = r₂ :=
  Eq.trans (eq_of_isSt_real h1) (eq_of_isSt_real h2).symm

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