exists_nnnorm_lt_one — Mathlib

English

There exists a nonzero element in the valuation ring whose NNReal norm is strictly between 0 and 1.

Русский

Существует ненулевой элемент в кольце оценки, чья NNReal-норма лежит строго между 0 и 1.

LaTeX

$$$$\exists x \in \mathcal{O}_K\; (0 < \|x\|_{\!+}) \land (\|x\|_{\!+} < 1).$$$$

Lean4

theorem exists_nnnorm_lt_one : ∃ x : 𝒪[K], 0 < ‖x‖₊ ∧ ‖x‖₊ < 1 :=
  exists_norm_coe_lt_one K

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