ext

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.ext

English

Two continuous linear equivalences are equal if their underlying maps are equal.

Русский

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

LaTeX

$$$ f = g \Rightarrow f.toFun = g.toFun $$$

Lean4

@[ext]
theorem ext {f g : M₁ ≃SL[σ₁₂] M₂} (h : (f : M₁ → M₂) = g) : f = g :=
  toLinearEquiv_injective <| LinearEquiv.ext <| congr_fun h

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

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

Разделы

Аффилиация

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