ofReal_inj

Mathlib.Data.Complex.Basic

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

← MathLib Explorer

English

The map z ↦ (z : ℂ) is injective on ℝ.

Русский

Отображение z ↦ (z : ℂ) инъективно на ℝ.

LaTeX

$$$\\\\forall z \\\\in \\\\mathbb{R}, \\\\forall w \\\\in \\\\mathbb{R}, \\\\big((z : \\\\mathbb{C}) = (w : \\\\mathbb{C}) \\\\Longrightarrow \\\\ z = w\\\\).$$$

Lean4

@[simp, norm_cast]
theorem ofReal_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=
  ⟨congrArg re, by apply congrArg⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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