isPiSystem_Ioo — Mathlib

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

Похожие утверждения