English
Let Ixx be as above and f,g be index maps into α. Then the family { S | ∃ i, ∃ j, p(f(i), g(j)) ∧ Ixx(f(i), g(j)) = S } is a π-system.
Русский
Пусть Ixx — как выше, а f,g — отображения индексов в α. Тогда множество { S | ∃ i, ∃ j, p(f(i), g(j)) ∧ Ixx(f(i), g(j)) = S } образует π-систему.
LaTeX
$$$$ \mathrm{IsPiSystem}\left(\{ S : \exists i, \exists j, p(f(i), g(j)) \land Ixx(f(i), g(j)) = S \}\right) $$$$
Lean4
theorem isPiSystem_Ixx {Ixx : α → α → Set α} {p : α → α → Prop} (Hne : ∀ {a b}, (Ixx a b).Nonempty → p a b)
(Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (f : ι → α) (g : ι' → α) :
@IsPiSystem α {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S} := by
simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)
