English
For rank-one valuations, ProperSpace K is equivalent to CompleteSpace K along with 𝒪[K] being a discrete valuation ring and finite residue field.
Русский
Для оценки ранга один, ProperSpace K эквивалентно CompleteSpace K и тому, что 𝒪[K] является дискретным кольцом оценки и конечным остаточным полем.
LaTeX
$$$$ \text{ProperSpace } K \iff (\text{CompleteSpace } K \land (\text{IsDiscreteValuationRing } 𝒪[K] \land Finite 𝓀[K])). $$$$
Lean4
theorem properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField
[(Valued.v : Valuation K Γ₀).RankOne] :
ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing 𝒪[K] ∧ Finite 𝓀[K] := by
simp only [properSpace_iff_compactSpace_integer,
compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField,
toNormedField.setOf_mem_integer_eq_closedBall, completeSpace_iff_isComplete_univ (α := 𝒪[K]),
Subtype.isComplete_iff, NormedField.completeSpace_iff_isComplete_closedBall, Set.image_univ,
Subtype.range_coe_subtype]
