pi — Mathlib · SciLib

English

If each C_i is a π-system, then the boxed construction formed by pi univ images is a π-system.

Русский

Если каждый C_i является π-системой, то образованный BOX-объект является π-системой.

LaTeX

$$$\\text{IsPiSystem}(\\pi\\ univ '' \\pi\\ univ (\\lambda i, C_i))$$$

Lean4

/-- Boxes formed by π-systems form a π-system. -/
theorem pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) : IsPiSystem (pi univ '' pi univ C) :=
  by
  rintro _ ⟨s₁, hs₁, rfl⟩ _ ⟨s₂, hs₂, rfl⟩ hst
  rw [← pi_inter_distrib] at hst ⊢; rw [univ_pi_nonempty_iff] at hst
  exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)

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