English
For y > 1 with y ≠ ∞, the open interval (0, ∞) equals the union over all integers n of the half-open intervals [y^n, y^{n+1}).
Русский
При y > 1 и y ≠ ∞ пределы: Ioo(0, ∞) равно объединению по всем n∈ℤ интервалов Ico(y^n, y^{n+1}).
LaTeX
$$$\\forall y \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; 1 < y \\land y \\neq \\top \\Rightarrow Ioo(0, \\top) = \\bigcup_{n \\in \\mathbb{Z}} Ico (y^n) (y^{n+1})$$$
Lean4
theorem Ioo_zero_top_eq_iUnion_Ico_zpow {y : ℝ≥0∞} (hy : 1 < y) (h'y : y ≠ ⊤) :
Ioo (0 : ℝ≥0∞) (∞ : ℝ≥0∞) = ⋃ n : ℤ, Ico (y ^ n) (y ^ (n + 1)) :=
by
ext x
simp only [mem_iUnion, mem_Ioo, mem_Ico]
constructor
· rintro ⟨hx, h'x⟩
exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y
· rintro ⟨n, hn, h'n⟩
constructor
· apply lt_of_lt_of_le _ hn
exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _
· apply lt_trans h'n _
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _
