withConstants_funMap_sumInr — Mathlib

English

The 0-ary function Sum.inr a interpreted by the new constants structure equals the constant map of a.

Русский

0-арный символ Sum.inr a интерпретируется как константа L.con a в новой структуре.

LaTeX

$$$ \\forall a \\in α, \\; @funMap (L[[α]]) M _ 0 (Sum.inr a : L[[α]].Functions 0) x = L.con a $$$

Lean4

@[simp]
theorem withConstants_funMap_sumInr {a : α} {x : Fin 0 → M} :
    @funMap (L[[α]]) M _ 0 (Sum.inr a : L[[α]].Functions 0) x = L.con a :=
  by
  rw [Unique.eq_default x]
  exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _

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