discreteTopology_of_bddAbove_range_norm

English

If the norms are bounded above on the range, the topology is discrete.

Русский

Если нормы на диапазоне ограничены сверху, топология дискретна.

LaTeX

$$$\text{BddAbove}(\mathrm{Set.range}(\lambda k: 𝕜 \mapsto \|k\|)) \Rightarrow \text{DiscreteTopology}(𝕜).$$$

Lean4

theorem discreteTopology_of_bddAbove_range_norm {𝕜 : Type*} [NormedField 𝕜] (h : BddAbove (Set.range fun k : 𝕜 ↦ ‖k‖)) :
    DiscreteTopology 𝕜 :=
  by
  refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_
  rintro ⟨_, rfl⟩
  obtain ⟨x, h⟩ := h
  obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x
  exact hk.not_ge (h (Set.mem_range_self k))

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