isPiSystem_Ioi_rat — Mathlib

English

The family of open rays Ioi(a) = (a, ∞) with rational endpoints a forms a Pi-system.

Русский

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

LaTeX

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

Lean4

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

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