funLike — Mathlib

English

There is a canonical FunLike instance for GroupNorm E, so elements of GroupNorm E act as real-valued functions on E.

Русский

Существует каноническая структура FunLike для GroupNorm E, так что элементы GroupNorm E выступают как вещественные функции на E.

LaTeX

$$$ \text{GroupNorm funLike} : \mathrm{GroupNorm}(E) \to (E \to \mathbb{R}) $$$

Lean4

@[to_additive]
instance funLike : FunLike (GroupNorm E) E ℝ where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _, _, _⟩, _⟩ := f; cases g; congr

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