comp_const — Mathlib

English

For f: α →o β and c ∈ γ, the composition (const β c) ∘ f equals the constant map α →o γ with value c.

Русский

Для отображения f: α →o β и фиксированного c ∈ γ композиция (const β c) ∘ f равна константному отображению α →o γ со значением c.

LaTeX

$$$ (\text{const}_{β} c) \cdot f = \text{const}_{γ} c $$$

Lean4

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

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