isPiSystem_Ioi — Mathlib

English

Let α be a linearly ordered set. The family of open rays (a, ∞) for a ∈ α forms a π-system; in particular, the intersection of two such rays is again of the same form: (max{a,b}, ∞).

Русский

Пусть α — линейно упорядоченное множество. Семейство лучей (a, ∞) с a ∈ α образует π-систему; пересечение любых двух лучей имеет вид (max(a,b), ∞).

LaTeX

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

Lean4

theorem isPiSystem_Ioi : IsPiSystem (range Ioi : Set (Set α)) :=
  @image_univ α _ Ioi ▸ isPiSystem_image_Ioi univ

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