English
If α is a complete space, then the complete copy of any open subset s of α is again a complete space.
Русский
Если α — полное пространство, то полное копирование любого открытого подмножества s внутри α является снова полным пространством.
LaTeX
$$$\text{CompleteSpace}(\mathrm{CompleteCopy}(s))$$$
Lean4
instance instCompleteSpace [CompleteSpace α] : CompleteSpace (CompleteCopy s) :=
by
refine Metric.complete_of_convergent_controlled_sequences ((1 / 2) ^ ·) (by simp) fun u hu ↦ ?_
have A : CauchySeq fun n => (u n).1 :=
by
refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
· exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le
· exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)
obtain ⟨x, xlim⟩ : ∃ x, Tendsto (fun n => (u n).1) atTop (𝓝 x) := cauchySeq_tendsto_of_complete A
by_cases xs : x ∈ s
· exact ⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩
obtain ⟨C, hC⟩ : ∃ C, ∀ n, 1 / infDist (u n).1 sᶜ < C :=
by
refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
rw [← sub_lt_iff_lt_add]
calc
_ ≤ |1 / infDist (u n).1 sᶜ - 1 / infDist (u 0).1 sᶜ| := le_abs_self _
_ = |1 / infDist (u 0).1 sᶜ - 1 / infDist (u n).1 sᶜ| := (abs_sub_comm _ _)
_ ≤ dist (u 0) (u n) := (le_add_of_nonneg_left dist_nonneg)
_ < (1 / 2) ^ 0 := hu 0 0 n le_rfl n.zero_le
have Cpos : 0 < C := lt_of_le_of_lt (div_nonneg zero_le_one infDist_nonneg) (hC 0)
have Hmem : ∀ {y}, y ∈ s ↔ 0 < infDist y sᶜ := fun {y} ↦ by
rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]; exact not_not.symm
have I : ∀ n, 1 / C ≤ infDist (u n).1 sᶜ := fun n ↦
by
have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
rw [div_le_iff₀' Cpos]
exact (div_le_iff₀ this).1 (hC n).le
have I' : 1 / C ≤ infDist x sᶜ :=
have : Tendsto (fun n => infDist (u n).1 sᶜ) atTop (𝓝 (infDist x sᶜ)) :=
((continuous_infDist_pt (sᶜ : Set α)).tendsto x).comp xlim
ge_of_tendsto' this I
exact absurd (Hmem.2 <| lt_of_lt_of_le (div_pos one_pos Cpos) I') xs
