English
There is a canonical equivalence between the space of dependent functions ∀a, P(e(a)) and the space ∀b, P(b), induced by transporting along e and its inverse.
Русский
Существует каноническое эквивалентное отображение между пространством зависимых функций ∀a, P(e(a)) и пространством ∀b, P(b), индуцированное переносом вдоль e и его обратного.
LaTeX
$$$\\forall a, P(e(a)) \\quad\\equiv\\quad \\forall b, P(b),\\quad$ через $f\\mapsto (b\\mapsto f(e^{-1}(b)))$ и $g\\mapsto (a\\mapsto g(e(a)))$.$$
Lean4
/-- Transporting dependent functions through an equivalence of the base,
expressed as a "simplification".
-/
def piCongrLeft : (∀ a, P (e a)) ≃ ∀ b, P b :=
(piCongrLeft' P e.symm).symm
