English
Rectangles formed by π-systems form a π-system; i.e., image2 (· ×ˢ ·) C D of two π-systems C and D is a π-system.
Русский
Прямоугольники, образованные π-системами, образуют π-систему; то есть образ2 (· ×ˢ ·) C D образует π-систему при C и D — π-системы.
LaTeX
$$$ IsPiSystem\ image2 (· ×ˢ ·) C D $$$
Lean4
/-- Rectangles formed by π-systems form a π-system. -/
theorem prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C) (hD : IsPiSystem D) :
IsPiSystem (image2 (· ×ˢ ·) C D) :=
by
rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst
rw [prod_inter_prod] at hst ⊢; rw [prod_nonempty_iff] at hst
exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)
