English
A Lebesgue number argument extends to products: an open cover of I×I has a monotone partition t of I with product subintervals contained in some cover set.
Русский
Аналогично для произведения: открытое покрытие I×I имеет монотонное разбиение на прямоугольные подпериоды, которые лежат внутри некоторого элемента покрытия.
LaTeX
$$Exists t : ℕ → I, t0 = 0 ∧ Monotone t ∧ ∃ n ∀ m ≥ n, t m = 1 ∧ ∀ n m ∃ i, Icc (t n) (t (n+1)) × Icc (t m) (t (m+1)) ⊆ c i$$
Lean4
theorem exists_monotone_Icc_subset_open_cover_unitInterval_prod_self {ι} {c : ι → Set (I × I)} (hc₁ : ∀ i, IsOpen (c i))
(hc₂ : univ ⊆ ⋃ i, c i) :
∃ t : ℕ → I,
t 0 = 0 ∧
Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n m, ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i :=
by
obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
have hδ := half_pos δ_pos
simp_rw [Subtype.ext_iff]
have h : (0 : ℝ) ≤ 1 := zero_le_one
refine ⟨addNSMul h (δ / 2), addNSMul_zero h, monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial
exact
⟨i, fun t ht ↦
hsub
(Metric.mem_ball.mpr <|
(max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <| abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <|
half_lt_self δ_pos)⟩
