English
A normed field is either discrete or nontrivially normed.
Русский
Нормированное поле либо дискретно, либо ненулево нормировано.
LaTeX
$$$\text{DiscreteTopology}(\mathbb{K}) \; \lor \; \exists h': \text{NontriviallyNormedField }\mathbb{K} \; (h'.toNormedField = h).$$$
Lean4
/-- A normed field is either nontrivially normed or has a discrete topology.
In the discrete topology case, all the norms are 1, by `norm_eq_one_iff_ne_zero_of_discrete`.
The nontrivially normed field instance is provided by a subtype with a proof that the
forgetful inheritance to the existing `NormedField` instance is definitionally true.
This allows one to have the new `NontriviallyNormedField` instance without data clashes. -/
theorem discreteTopology_or_nontriviallyNormedField (𝕜 : Type*) [h : NormedField 𝕜] :
DiscreteTopology 𝕜 ∨ Nonempty ({ h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h }) :=
by
by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
· exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩
· simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero]
refine Or.inl ⟨1, zero_lt_one, ?_⟩
contrapose! H
refine
H.imp
?_
-- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
simp +contextual [ne_of_lt]
