ofReal_inj

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_inj

English

For all z,w ∈ ℝ, ofReal z = ofReal w iff z = w.

Русский

Для всех z,w ∈ ℝ верно, что ofReal z = ofReal w тогда и только тогда, когда z = w.

LaTeX

$$$\forall z,w \in \mathbb{R},\ (\mathrm{OfReal}\, z) = (\mathrm{OfReal}\, w) \iff z = w$$$

Lean4

@[norm_cast]
theorem ofReal_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w :=
  algebraMap.coe_inj

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru