eq_comp_symm — Mathlib

English

For e: α ≃ β, f: β → γ, g: α → γ, equality f = g ∘ e^{-1} holds if and only if f ∘ e = g.

Русский

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

LaTeX

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

Lean4

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

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