mixedSpaceOfRealSpace_apply — Mathlib

English

The mixedSpaceOfRealSpace real-space embedding maps x to a real-space element whose components are given by x evaluated at the first coordinate.

Русский

Отображение real-space в смешанное пространство отображает x в элемент real-space, компоненты которого задаются как x, примененная к первой координате.

LaTeX

$$$\text{mixedSpaceOfRealSpace}(x) = \langle \lambda w. x(w.1), \lambda w. x(w.1)\rangle.$$$

Lean4

theorem mixedSpaceOfRealSpace_apply (x : realSpace K) : mixedSpaceOfRealSpace x = ⟨fun w ↦ x w.1, fun w ↦ x w.1⟩ :=
  rfl

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