ι_π_eq_id — Mathlib

English

For a family f: β → C with a product, the composite Pi.ι f b ≫ Pi.π f b equals the identity on f(b).

Русский

Для семейства f: β → C с произведением композиция Pi.ι f b ≫ Pi.π f b равна тождественному отображению на f(b).

LaTeX

$$$\Pi\!\iota_f(b) \;\circ\; \Pi\!\pi_f(b) = \mathrm{id}_{f(b)}$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_π_eq_id (b : β) : Pi.ι f b ≫ Pi.π f b = 𝟙 _ := by simp [Pi.ι]

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