symm_comp_eq

Mathlib.Topology.Algebra.ContinuousMonoidHom

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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