properSpace_iff_compactSpace_integer

English

For a rank-one valuation, K is a proper space if and only if 𝒪[K] is compact.

Русский

Для оценки ранга единицы пространство K является правильным тогда и только тогда, когда 𝒪[K] компактно.

LaTeX

$$$$ \text{ProperSpace } K \iff \text{CompactSpace } 𝒪[K]. $$$$

Lean4

theorem properSpace_iff_compactSpace_integer [(Valued.v : Valuation K Γ₀).RankOne] :
    ProperSpace K ↔ CompactSpace 𝒪[K] :=
  by
  simp only [← isCompact_univ_iff, Subtype.isCompact_iff, Set.image_univ, Subtype.range_coe_subtype,
    toNormedField.setOf_mem_integer_eq_closedBall]
  constructor <;> intro h
  · exact isCompact_closedBall 0 1
  · suffices LocallyCompactSpace K from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace K
    exact IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup h <| Metric.closedBall_mem_nhds 0 zero_lt_one

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