comp_const — Mathlib

English

Composing any map f with the constant map at z is the same as taking the constant map at the image z under f.

Русский

Собирая любую стрелку f с константной картой в z, получаем ту же константную карту в образе z через f.

LaTeX

$$$f \;\gg\; \text{const}_z = \text{const}_{f(z)}$$$

Lean4

@[simp]
theorem comp_const {X Y Z : SSet.{u}} (f : X ⟶ Y) (z : Z _⦋0⦌) : f ≫ const z = const z :=
  rfl

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