pi_singletons — Mathlib

English

If t(a) are singletons, then s.pi t is a singleton containing the unique function a ↦ f(a).

Русский

Если каждый t(a) — синглетон, тогда s.pi t — синглетон, содержащий единственную функцию a ↦ f(a).

LaTeX

$$$ (s.\\pi (\\lambda a, {f(a)})) = {\\lambda a, b. f(a)}. $$$

Lean4

theorem pi_singletons {β : Type*} (s : Finset α) (f : α → β) : (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a} :=
  by
  rw [eq_singleton_iff_unique_mem]
  constructor
  · simp
  intro a ha
  ext i hi
  rw [mem_pi] at ha
  simpa using ha i hi

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