isPiSystem_Icc — Mathlib

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

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