eq_symm_comp

Mathlib.Topology.Algebra.ContinuousMonoidHom

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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