piCongrLeft_symm_apply — Mathlib

English

The inverse of piCongrLeft acts by precomposition with the index bijection: the inverse map sends a function g to g ∘ e.

Русский

Обратное к piCongrLeft действует через предкомпозицию с биекцией индексов: обратная карта отправляет функцию g в g ∘ e.

LaTeX

$$$(\\pi\\text{CongrLeft} \\\\ e)^{-1} = (\\lambda g, g \\circ e)$$$

Lean4

@[simp]
theorem piCongrLeft_symm_apply {ι ι' : Type*} {X : ι' → Type*} [∀ j, UniformSpace (X j)] (e : ι ≃ ι') :
    ⇑(piCongrLeft (β := X) e).symm = (· <| e ·) :=
  rfl

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