toReal_injective — Mathlib

English

The map Real.Angle.toReal is injective: if toReal(α) = toReal(β) then α = β.

Русский

Отображение Real.Angle.toReal инъективно: если toReal(α) = toReal(β), то α = β.

LaTeX

$$$\forall \theta, \psi:\; \operatorname{toReal}(\theta) = \operatorname{toReal}(\psi) \Rightarrow \theta = \psi$$$

Lean4

theorem toReal_injective : Function.Injective toReal :=
  by
  intro θ ψ h
  induction θ using Real.Angle.induction_on
  induction ψ using Real.Angle.induction_on
  simpa [toReal_coe, toIocMod_eq_toIocMod, zsmul_eq_mul, mul_comm _ (2 * π), ← angle_eq_iff_two_pi_dvd_sub,
    eq_comm] using h

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