coe

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.Simps.coe

English

Two continuous semilinear maps are equal if they agree on every point.

Русский

Два непрерывных семилинейных отображения равны, если они совпадают в каждой точке.

LaTeX

$$$\forall x\; (f x = g x) \Rightarrow f=g$$$

Lean4

/-- See Note [custom simps projection]. -/
def coe (h : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂ :=
  h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru