reindex_inv_π — Mathlib

English

The inverse part of reindexing gives the expected projection relation.

Русский

Обратная часть реиндексации задаёт ожидаемое отношение проекций.

LaTeX

$$$(\Pi\text{reindex }\varepsilon f)^{\mathrm{inv}} \circ \Pi (f\circ \varepsilon) b = \Pi f (\varepsilon b)$$$

Lean4

@[reassoc (attr := simp)]
theorem reindex_inv_π (b : β) : (Pi.reindex ε f).inv ≫ Pi.π (f ∘ ε) b = Pi.π f (ε b) := by simp [Iso.inv_comp_eq]

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