funUnique — Mathlib

English

Equiv.funUnique can be realized as an isometry equivalence: there is an isometry between ι → α and α when ι is Unique and Finite.

Русский

Equiv.funUnique реализуется как изометрическое эквивалентное отображение: существует изометрия между ι → α и α, если ι уникально и конечен.

LaTeX

$$$ (\iota \to α) \simeq_i α \quad\text{for Unique } \iota,\ Fintype \iota$$$

Lean4

/-- `Equiv.funUnique` as an `IsometryEquiv`. -/
@[simps!]
def funUnique [Unique ι] [Fintype ι] : (ι → α) ≃ᵢ α
    where
  toEquiv := Equiv.funUnique ι α
  isometry_toFun x hx := by simp [edist_pi_def, Finset.univ_unique, Finset.sup_singleton]

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