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