postcomp — Mathlib

English

If F is eventually constant to i0, then postcomposing with morphisms f: i0 → j yields FIsEventuallyConstantTo j.

Русский

Если F константен относительно i0, то посткомпозиция с f: i0 → j сохраняет константность относительно j.

LaTeX

$$$\text{IsEventuallyConstantFrom}(j)\;\text{for } f: i_0 \to j$$$

Lean4

theorem postcomp {j : J} (f : i₀ ⟶ j) : F.IsEventuallyConstantFrom j := fun _ φ ↦ h.isIso_map φ f

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