piCongrLeft_apply_apply — Mathlib

English

Applying piCongrLeft and then evaluating at e i recovers the original i-th component: (piCongrLeft e x)(e i) = x(i).

Русский

Применение piCongrLeft и затем вывод по значению в e i восстанавливает i-ую компоненту: (piCongrLeft e x)(e i) = x(i).

LaTeX

$$$\\pi\\text{CongrLeft}\\ e\\ x (e\\,i) = x\\,i$$$

Lean4

@[simp]
theorem piCongrLeft_apply_apply {ι ι' : Type*} {X : ι' → Type*} [∀ j, UniformSpace (X j)] (e : ι ≃ ι')
    (x : ∀ i, X (e i)) i : piCongrLeft e x (e i) = x i :=
  Equiv.piCongrLeft_apply_apply ..

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