coe_inj

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.coe_inj

English

For z,w in UnitDisc, (z : ℂ) = w if and only if z = w.

Русский

Для z,w ∈ UnitDisc верно: (z : ℂ) = w ⇒ z = w и наоборот.

LaTeX

$$$ (z : \\mathbb{C}) = w \\\\Leftrightarrow z = w \\quad (z,w \\in \\mathbb{D}) $$$

Lean4

@[simp, norm_cast]
theorem coe_inj {z w : 𝔻} : (z : ℂ) = w ↔ z = w :=
  Subtype.val_inj

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

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

Разделы

Аффилиация

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