pi_const_singleton — Mathlib

English

Pi over s with constant value i is a singleton containing the constant function a ↦ i.

Русский

Pi над s с константным значением i образует синглетон из константной функции a ↦ i.

LaTeX

$$$ (s.\\pi (\\lambda a, {i})) = {\\lambda a, h. i}. $$$

Lean4

theorem pi_const_singleton {β : Type*} (s : Finset α) (i : β) : (s.pi fun _ => ({ i } : Finset β)) = {fun _ _ => i} :=
  pi_singletons s fun _ => i

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