const_comp — Mathlib

English

For any f: α →o β and any c ∈ γ, the composition of the constant map (β →o γ) sending every β to c with f yields the constant map α →o γ sending every α to c.

Русский

Для любого f: α →o β и любого c ∈ γ композиция константного отображения β →o γ, отправляющего γ в c, с f даёт константное отображение α →o γ, отправляющее каждое α в c.

LaTeX

$$$ (\text{const}_{β} c) \circ f = \text{const}_{α} c. $$$

Lean4

@[simp]
theorem const_comp (f : α →o β) (c : γ) : (const β c).comp f = const α c :=
  rfl

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