of_forall_le_norm' — Mathlib

English

If there exists r>0 such that for all x ≠ 1, r ≤ ‖x‖, then the topology on E is discrete.

Русский

Если существует r>0 такое, что для всякого x ≠ 1 выполняется r ≤ ‖x‖, то топология на E дискрета.

LaTeX

$$$\forall r>0, \forall x\neq 1, r \le \|x\| \Rightarrow DiscreteTopology E$$$

Lean4

@[to_additive of_forall_le_norm]
theorem of_forall_le_norm' (hpos : 0 < r) (hr : ∀ x : E, x ≠ 1 → r ≤ ‖x‖) : DiscreteTopology E :=
  .of_forall_le_dist hpos fun x y hne ↦ by
    simp only [dist_eq_norm_div]
    exact hr _ (div_ne_one.2 hne)

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