isPiSystem_Iic_rat — Mathlib

English

The family of half-open intervals Iic(a) = (−∞, a] with rational a forms a Pi-system.

Русский

Семейство полузакрытых интервалов Iic(a) = (−∞, a] с рациональными a образует Pi-систему.

LaTeX

$$$$\text{IsPiSystem}\left(\bigcup_{a \in \mathbb{Q}} \{ Iic(a) \} \right)$$$$

Lean4

theorem isPiSystem_Iic_rat : IsPiSystem (⋃ a : ℚ, {Iic (a : ℝ)}) :=
  by
  convert isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)
  ext x
  simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

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