English
If s is a Pi-system, then for any t1,t2 with t1,t2 ∈ generate(s), we have t1 ∩ t2 ∈ generate(s).
Русский
Если s — π-система, то для любых t1,t2 ∈ generate(s) выполняется t1 ∩ t2 ∈ generate(s).
LaTeX
$$$ IsPiSystem\, s \Rightarrow \forall {t_1 t_2},\ (t_1 \in generate(s) \land t_2 \in generate(s)) \Rightarrow (t_1 \cap t_2) \in generate(s). $$$
Lean4
theorem generate_inter {s : Set (Set α)} (hs : IsPiSystem s) {t₁ t₂ : Set α} (ht₁ : (generate s).Has t₁)
(ht₂ : (generate s).Has t₂) : (generate s).Has (t₁ ∩ t₂) :=
have : generate s ≤ (generate s).restrictOn ht₂ :=
generate_le _ fun s₁ hs₁ =>
have : (generate s).Has s₁ := GenerateHas.basic s₁ hs₁
have : generate s ≤ (generate s).restrictOn this :=
generate_le _ fun s₂ hs₂ =>
show (generate s).Has (s₂ ∩ s₁) from
(s₂ ∩ s₁).eq_empty_or_nonempty.elim (fun h => h.symm ▸ GenerateHas.empty) fun h =>
GenerateHas.basic _ <| hs _ hs₂ _ hs₁ h
have : (generate s).Has (t₂ ∩ s₁) := this _ ht₂
show (generate s).Has (s₁ ∩ t₂) by rwa [inter_comm]
this _ ht₁
