English
For f: ι → α and g: ι' → α, the family { S | ∃ l,u with f(l) < g(u) ∧ Ioo(f(l), g(u)) = S } is a π-system.
Русский
Для функций f: ι → α и g: ι' → α множество { S | ∃ l,u с f(l) < g(u) и Ioo(f(l), g(u)) = S } является π-системой.
LaTeX
$$$$ \mathrm{IsPiSystem}\left(\{ S : \exists i, \exists j, f(i) < g(j) \land Ioo(f(i), g(j)) = S \}\right) $$$$
Lean4
theorem isPiSystem_Ioo (f : ι → α) (g : ι' → α) : @IsPiSystem α {S | ∃ l u, f l < g u ∧ Ioo (f l) (g u) = S} :=
isPiSystem_Ixx (Ixx := Ioo) (fun ⟨_, hax, hxb⟩ => hax.trans hxb) Ioo_inter_Ioo f g