pi_mulSingle_eq — Mathlib

English

In a subsingleton index type I with a single element i, for any x in α, Pi.mulSingle i x is the constant function taking value x.

Русский

Для элементов i в попарном индексе I, где I — одноэлементный, любой x ∈ α даёт Pi.mulSingle i x — константную функцию, принимающую значение x.

LaTeX

$$$ \forall i, x,\; \mathrm{Pi.mulSingle}\ i\ x = \lambda j, x$$$

Lean4

@[to_additive]
theorem pi_mulSingle_eq {α : Type*} [DecidableEq I] [Subsingleton I] [One α] (i : I) (x : α) :
    Pi.mulSingle i x = fun _ => x :=
  funext fun j => by rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

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