English
Let β be an index set, and for each j in β let f_j and g_j be types with maps α_j : f_j → g_j. For b ∈ β and x ∈ ∏_{j∈β} f_j, the b-th component of Pi.map α applied to x equals α_b applied to the b-th component of x.
Русский
Пусть β — множество индексов, для каждого j ∈ β даны типы f_j, g_j и отображения α_j: f_j → g_j. Для b ∈ β и x ∈ ∏_{j∈β} f_j верно: компонентa в позиции b у Pi.map α applied к x равна α_b применённому к компоненте x в позиции b.
LaTeX
$$$$ (\\Pi\\pi g b)(\\Pi map α\\ x) = α_b\\big((\\Pi\\pi f b) x\\big) $$$$
Lean4
/-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`,
with specialized universes. -/
theorem pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
(Pi.π g b : ∏ᶜ g → g b) (Pi.map α x) = α b ((Pi.π f b : ∏ᶜ f → f b) x) := by simp
