isPiSystem_Ioo_rat — Mathlib

English

The family of open intervals with rational endpoints, Ioo(a, b) with a,b ∈ ℚ and a < b, forms a Pi-system. In particular, the union over all such a,b of the singleton {Ioo(a,b)} is a Pi-system.

Русский

Семейство открытых интервалов с рациональными концами Ioo(a,b) с a,b ∈ ℚ, a < b, образует Pi-систему.

LaTeX

$$$$\\text{IsPiSystem}\\left(\\bigcup_{a,b \\in \\mathbb{Q}, a < b} \\{ Ioo(a,b) \}\\right)$$$$

Lean4

theorem isPiSystem_Ioo_rat : IsPiSystem (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)}) :=
  by
  convert isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
  ext x
  simp [eq_comm]

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