apply — Mathlib

English

Let e be a continuous linear equivalence between topological modules M1 and M2. Then the action of e on any element x ∈ M1 is exactly the image of x under e, i.e., the function part of e coincides with its evaluation.

Русский

Пусть e — непрерывное линейное эквивалентное отображение между топологическими модулями M1 и M2. Тогда действие e на элемент x ∈ M1 есть именно образ x под действием e, то есть функция, задаваемая e, совпадает с её значением на x.

LaTeX

$$$\\forall x \\in M_1:\\; e(x) = e(x)$$$

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def apply (h : M₁ ≃SL[σ₁₂] M₂) : M₁ → M₂ :=
  h

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