funUnique — Mathlib

English

If ι has a unique element, then ι → M is continuously linearly equivalent to M.

Русский

Если множество ι имеет уникальный элемент, то пространство функций ι → M эквивалентно M непрерывно-линейно.

LaTeX

$$$ (ι \\to M) \\simeq_L[R] M$$$

Lean4

/-- If `ι` has a unique element, then `ι → M` is continuously linear equivalent to `M`. -/
def funUnique : (ι → M) ≃L[R] M :=
  { Homeomorph.funUnique ι M with toLinearEquiv := LinearEquiv.funUnique ι R M }

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