const_comp — Mathlib

English

Composing a map with a constant map yields a constant map with the same constant value.

Русский

Составление отображения с константным отображением даёт константное отображение с тем же значением.

LaTeX

$$$(\text{const }\beta(c)).\circ f = \text{const }\alpha(c)$$$

Lean4

@[simp]
theorem const_comp (c : γ) (f : C(α, β)) : (const β c).comp f = const α c :=
  ext fun _ => rfl

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