univ_pi_singleton — Mathlib

English

The pi over the full universe with singleton values equals the singleton set containing the function f.

Русский

π над вселенной с единичными значениями равно множеству, содержащему единственную функцию f.

LaTeX

$$$ \pi \mathrm{univ} t = \{ f \} $ when t i = \{ f(i) \} for all i.$$

Lean4

theorem univ_pi_singleton (f : ∀ i, α i) : (pi univ fun i => {f i}) = ({ f } : Set (∀ i, α i)) :=
  ext fun g => by simp [funext_iff]

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