funLike — Mathlib

English

GroupSeminorm E carries a function-like structure: each p ∈ GroupSeminorm E acts as a function p: E → ℝ, and equality is detected by their values on all inputs.

Русский

GroupSeminorm E имеет структуру, подобную функции: каждый p ∈ GroupSeminorm E действует как функция p: E → ℝ, и равенство определяется значениями на всех аргументах.

LaTeX

$$\\text{GroupSeminorm } E \\text{ is function-like with } \\text{coe } p := p.toFun, \\text{ and } p.toFun = q.toFun \\Rightarrow p = q$$

Lean4

@[to_additive]
instance funLike : FunLike (GroupSeminorm E) E ℝ
    where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; congr

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