isPiSystem_Ici_rat — Mathlib

English

The family of half-infinite rays Ici(a) = [a, ∞) with rational a forms a Pi-system.

Русский

Семейство лучей Ici(a) = [a, ∞) с рациональными a образует Pi-систему.

LaTeX

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

Lean4

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

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