comp_symm_eq

Mathlib.Topology.Algebra.ContinuousMonoidHom

URI: https://scilib.ai/kg/mathlib#ContinuousMulEquiv.comp_symm_eq

English

For e: M ≃ₜ* N, f: N → α and g: M → α, g ∘ e^{-1} = f iff g = f ∘ e.

Русский

Для e: M ≃ₜ* N, f: N → α и g: M → α верно: g ∘ e^{-1} = f тогда и только тогда, когда g = f ∘ e.

LaTeX

$$$g \circ e^{-1} = f \iff g = f \circ e$$$

Lean4

@[to_additive]
theorem comp_symm_eq {α : Type*} (e : M ≃ₜ* N) (f : N → α) (g : M → α) : g ∘ e.symm = f ↔ g = f ∘ e :=
  e.toEquiv.comp_symm_eq f g

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

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

Разделы

Аффилиация

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