injective_mixedSpaceOfRealSpace — Mathlib

English

The map from real-space K to mixed-space K is injective: if mixedSpaceOfRealSpace x = mixedSpaceOfRealSpace y then x = y.

Русский

Отображение real-space в смешанное пространство инъективно: равенство изображений значит равенство исходных объектов.

LaTeX

$$$\forall x,y:\, realSpace(K),\ (mixedSpaceOfRealSpace\;x = mixedSpaceOfRealSpace\;y) \Rightarrow x = y.$$$

Lean4

theorem injective_mixedSpaceOfRealSpace : Function.Injective (mixedSpaceOfRealSpace : realSpace K → mixedSpace K) :=
  by
  refine (injective_iff_map_eq_zero mixedSpaceOfRealSpace).mpr fun _ h ↦ ?_
  rw [mixedSpaceOfRealSpace_apply, Prod.mk_eq_zero, funext_iff, funext_iff] at h
  ext w
  obtain hw | hw := isReal_or_isComplex w
  · exact h.1 ⟨w, hw⟩
  · exact Complex.ofReal_inj.mp <| h.2 ⟨w, hw⟩

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