isPiSystem_Ioc — Mathlib

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

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