coe_linearEquiv — Mathlib

English

The underlying function of the linearEquiv is the same as mapDomain: the coercion to function agrees with mapDomain.

Русский

Функциональное представление линейного эквивалента совпадает с mapDomain по функции.

LaTeX

$$$\\forall f: α\\simeq α',\\; \\big( (linearEquiv M R f) : (α→₀ M) \\to α'→₀ M \\big) = mapDomain f$$$

Lean4

@[simp]
theorem coe_linearEquiv (f : α ≃ α') : ⇑(linearEquiv M R f) = mapDomain f :=
  rfl

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