English
There exists a construction mk' that equips R with a valuation-derived uniform structure without a preferred separate UniformSpace.
Русский
Существует конструктор mk', который снабжает кольцо R структурой униформности, полученной из оценки, без явно заданного пространства равномерности.
LaTeX
$$def mk' (v : Valuation R Γ₀) : Valued R Γ₀$$
Lean4
/-- Alternative `Valued` constructor for use when there is no preferred `UniformSpace` structure. -/
def mk' (v : Valuation R Γ₀) : Valued R Γ₀ :=
{ v
toUniformSpace := @IsTopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
toIsUniformAddGroup := @isUniformAddGroup_of_addCommGroup _ _ v.subgroups_basis.topology _
is_topological_valuation :=
by
letI := @IsTopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
intro s
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
exact exists_congr fun γ => by rw [true_and]; rfl }
