eq_conj — Mathlib

English

If ε1: α ≃ α', ε2: β' ≃ β, f: α → β, f': α' → β', then ε2⁻¹ ∘ f ∘ ε1⁻¹ = f' iff f = ε2 ∘ f' ∘ ε1.

Русский

Если ε1: α ≃ α', ε2: β' ≃ β, f: α→β, f': α'→β', тогда ε2⁻¹ ∘ f ∘ ε1⁻¹ = f' тогда и только если f = ε2 ∘ f' ∘ ε1.

LaTeX

$$$\\varepsilon_2^{-1} \\circ f \\circ \\varepsilon_1^{-1} = f' \\iff f = \\varepsilon_2 \\circ f' \\circ \\varepsilon_1$$$

Lean4

theorem eq_conj {α α' β β' : Sort*} (ε₁ : α ≃ α') (ε₂ : β' ≃ β) (f : α → β) (f' : α' → β') :
    ε₂.symm ∘ f ∘ ε₁.symm = f' ↔ f = ε₂ ∘ f' ∘ ε₁ := by rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]

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