English
A metric space α is second countable if there exists a discretization data—encodable β, a map F: α→β with the property that for all x,y, F(x)=F(y) implies dist(x,y)≤ε for every ε>0—then α has a countable base.
Русский
Метрическое пространство α имеет счетную базу, если существует дискретизация: кодируемый β и отображение F: α→β такое, что для любых x,y с F(x)=F(y) выполняется dist(x,y)≤ε для каждого ε>0; тогда топология α счетна.
LaTeX
$$SecondCountableTopology(α)$$
Lean4
/-- A metric space is second countable if one can reconstruct up to any `ε>0` any element of the
space from countably many data. -/
theorem secondCountable_of_countable_discretization {α : Type u} [PseudoMetricSpace α]
(H : ∀ ε > (0 : ℝ), ∃ (β : Type*) (_ : Encodable β) (F : α → β), ∀ x y, F x = F y → dist x y ≤ ε) :
SecondCountableTopology α :=
by
refine secondCountable_of_almost_dense_set fun ε ε0 => ?_
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
let Finv := rangeSplitting F
refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩
let x' := Finv ⟨F x, mem_range_self _⟩
have : F x' = F x := apply_rangeSplitting F _
exact ⟨x', mem_range_self _, hF _ _ this.symm⟩
