eq_symm_comp — Mathlib

English

For e: α ≃ β, f: γ → α, this states f = e^{-1} ∘ g iff e ∘ f = g.

Русский

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

LaTeX

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

Lean4

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

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