isPiSystem_Ico — Mathlib

English

For f: ι → α and g: ι' → α, the family { S | ∃ i,j, f(i) < g(j) ∧ Ico(f(i), g(j)) = S } is a π-system.

Русский

Для функций f: ι → α и g: ι' → α множество { S | ∃ i,j, f(i) < g(j) ∧ Ico(f(i), g(j)) = S } образует π-систему.

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ S : \exists i, \exists j, f(i) < g(j) \land Ico(f(i), g(j)) = S \}\right) $$$$

Lean4

theorem isPiSystem_Ico (f : ι → α) (g : ι' → α) : @IsPiSystem α {S | ∃ i j, f i < g j ∧ Ico (f i) (g j) = S} :=
  isPiSystem_Ixx (Ixx := Ico) (fun ⟨_, hax, hxb⟩ => hax.trans_lt hxb) Ico_inter_Ico f g

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