isPiSystem_Ici — Mathlib

English

The family { Ici(a) : a ∈ α } is a π-system; equivalently, the range of Ici forms a π-system.

Русский

Семейство { [a, ∞) : a ∈ α } образует π-систему; эквивалентно диапазону Ici образуется π-система.

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ Ici(a) : a \in \alpha \}\right) $$$$

Lean4

theorem isPiSystem_Ici : IsPiSystem (range Ici : Set (Set α)) :=
  @image_univ α _ Ici ▸ isPiSystem_image_Ici univ

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