coe_eq_coe — Mathlib

English

The equality of embedded real numbers in the hyperreals is equivalent to equality of the reals.

Русский

Равенство вложенных действительных чисел в гиперреальных эквивалентно равенству самих чисел.

LaTeX

$$$\forall x,y \in \mathbb{R}, (x : \mathbb{R}^*) = y \Leftrightarrow x = y$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_coe {x y : ℝ} : (x : ℝ*) = y ↔ x = y :=
  Germ.const_inj

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