univ_pi_eq_iInter

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.univ_pi_eq_iInter

English

If t is a family of subsets indexed by α, then univ.pi t equals the intersection over i of eval i preimage of t i.

Русский

Если t — множество подмножеств, то univ.pi t = ⋂ i, eval i^{-1}(t i).

LaTeX

$$$$ \mathrm{univ}.\pi t = \bigcap_{i} \operatorname{eval}_{i}^{-1}(t(i)) $$$$

Lean4

theorem univ_pi_eq_iInter (t : ∀ i, Set (π i)) : pi univ t = ⋂ i, eval i ⁻¹' t i := by
  simp only [pi_def, iInter_true, mem_univ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru