subsingleton_univ_pi — Mathlib

English

If every t_i is a Subsingleton, then the universal pi is a Subsingleton.

Русский

Если каждый t_i является одиночным подмножеством, то единичное произведение по нулю индексов также является одиночным.

LaTeX

$$$ (univ.pi t).Subsingleton = \text{Subsingleton if all } (t i).Subsingleton $$$

Lean4

theorem subsingleton_univ_pi (ht : ∀ i, (t i).Subsingleton) : (univ.pi t).Subsingleton := fun _f hf _g hg ↦
  funext fun i ↦ (ht i) (hf _ <| mem_univ _) (hg _ <| mem_univ _)

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