eq_comp_symm

Mathlib.Topology.Algebra.ContinuousMonoidHom

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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