comp_symm_eq

Mathlib.Logic.Equiv.Defs

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

English

For e: α ≃ β, f: γ → α, g: γ → β, g ∘ e.symm = f iff g = e ∘ f.

Русский

Для e: α ≃ β, f: γ → α, g: γ → β, g ∘ e^{-1} = f тогда и только тогда, когда g = e ∘ f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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