piCongrLeft_apply_apply — Mathlib

English

Let e be a bijection ι ≃ ι′ and β a family of spaces β i′. For any x : (i : ι) → β (e i) and i : ι, the evaluation of the induced piCongrLeft map at i matches the component x i; i.e., the left-congruence left-applied to x and then evaluated at e i equals x i.

Русский

Пусть e — биекция ι ≃ ι′ и β — семейство пространств β i′. Для любого x : (i : ι) → β (e i) и индекса i верно, что соответствующая формула лево-конгруэнтности даёт x i при применении к e i.

LaTeX

$$$\\pi\\text{-CongrLeft} (fun\\ i' \\mapsto \\beta i')\\ e\\ x\\ (e\\ i) = x\\ i$$$

Lean4

theorem piCongrLeft_apply_apply {ι ι' : Type*} (e : ι ≃ ι') {β : ι' → Type*} [∀ i', MeasurableSpace (β i')]
    (x : (i : ι) → β (e i)) (i : ι) : piCongrLeft (fun i' ↦ β i') e x (e i) = x i := by
  rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]

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