piCongrLeft_symm_apply — Mathlib

English

For f : ∀ a, P (e a) and b : β, (piCongrLeft P e) f b equals e.apply_symm_apply b transported to f (e.symm b).

Русский

Для f : ∀ a, P (e a) и b : β, имеет место (piCongrLeft P e) f b = e.apply_symm_apply b транспорированное к f (e.symm b).

LaTeX

$$$(\\pi_{\\mathrm{CongrLeft}} P e) f b = e.\\mathrm{apply\\_symm\\_apply} b \\;\\; \\text{transport} \\; f (e.\\mathrm{symm} b).$$$

Lean4

@[simp]
theorem piCongrLeft_symm_apply (g : ∀ b, P b) (a : α) : (piCongrLeft P e).symm g a = g (e a) :=
  piCongrLeft'_apply P e.symm g a

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