English
For f: ι → α and g: ι' → α, the family { S | ∃ i,j, f(i) ≤ g(j) ∧ Icc(f(i), g(j)) = S } is a π-system.
Русский
Для функций f: ι → α и g: ι' → α множество { S | ∃ i,j, f(i) ≤ g(j) ∧ Icc(f(i), g(j)) = S } образует π-систему.
LaTeX
$$$$ \mathrm{IsPiSystem}\left(\{ S : \exists i, \exists j, f(i) \le g(j) \land Icc(f(i), g(j)) = S \}\right) $$$$
Lean4
theorem isPiSystem_Icc (f : ι → α) (g : ι' → α) : @IsPiSystem α {S | ∃ i j, f i ≤ g j ∧ Icc (f i) (g j) = S} :=
isPiSystem_Ixx (Ixx := Icc) nonempty_Icc.1 (by exact Icc_inter_Icc) f g