ext

Mathlib.Topology.Algebra.Algebra.Equiv

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

English

Two continuous algebra equivalences are equal if their underlying functions are equal.

Русский

Две непрерывные алгебраические эквиваленты равны, если их функции совпадают.

LaTeX

$$ext {f g : ContinuousAlgEquiv R A B} (h : ⇑f = ⇑g) : f = g$$

Lean4

@[ext]
theorem ext {f g : A ≃A[R] B} (h : ⇑f = ⇑g) : f = g :=
  toAlgEquiv_injective <| AlgEquiv.ext <| congr_fun h

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

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

Разделы

Аффилиация

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