completeSpace — Mathlib

English

The product space ∀n E_n is a complete space when each E_n is discrete and complete in its own right.

Русский

Произведение ∀n E_n является полным пространством, когда каждое E_n является полным пространством.

LaTeX

$$$$ \text{CompleteSpace}\bigl( (n \mapsto E_n) \bigr) $$$$

Lean4

protected theorem completeSpace : CompleteSpace (∀ n, E n) :=
  by
  refine Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) ?_
  intro u hu
  refine ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩
  refine tendsto_const_nhds.congr' ?_
  filter_upwards [Filter.Ici_mem_atTop i] with n hn
  exact apply_eq_of_dist_lt (hu i i n le_rfl hn) le_rfl

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