symm_comp_eq

Mathlib.Logic.Equiv.Defs

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

English

Equivalently, e^{-1} ∘ g = f if and only if g = e ∘ f.

Русский

Эквивалентно: e^{-1} ∘ g = f тогда и только тогда, когда g = e ∘ f.

LaTeX

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

Lean4

theorem symm_comp_eq {α β γ} (e : α ≃ β) (f : γ → α) (g : γ → β) : e.symm ∘ g = f ↔ g = e ∘ f :=
  ((Equiv.refl γ).arrowCongr e).symm_apply_eq

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

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

Разделы

Аффилиация

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