isPiSystem_image_Iic — Mathlib

English

For any subset s of α, the family { Iic(a) : a ∈ s } is a π-system, where Iic(a) = (−∞, a].

Русский

Для любого подмножества s ⊆ α семейство { (−∞, a] : a ∈ s } образует π-систему, где Iic(a) = (−∞, a].

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ Iic(a) : a \in s \}\right) $$$$

Lean4

theorem isPiSystem_image_Iic (s : Set α) : IsPiSystem (Iic '' s) :=
  by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
  exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩

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