eq_re_iff_mem_range_coe — Mathlib

English

An element equals its real part iff it lies in the range of the canonical embedding of R into H.

Русский

Элемент равен своей вещественной части тогда и только тогда, когда он лежит в образе канонического вложения R в H.

LaTeX

$$$a = a.re \iff a \in \mathrm{Range}(\mathrm{coe} : R \to \mathbb{H}(R,c_1,c_2,c_3))$$$

Lean4

theorem eq_re_iff_mem_range_coe {a : ℍ[R,c₁,c₂,c₃]} : a = a.re ↔ a ∈ Set.range (coe : R → ℍ[R,c₁,c₂,c₃]) :=
  ⟨fun h => ⟨a.re, h.symm⟩, fun ⟨_, h⟩ => eq_re_of_eq_coe h.symm⟩

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