nndist_one_right — Mathlib

English

The uniformity on E has a basis given by distance-based sets: {p: E×E | ‖p.fst / p.snd‖ < ε}.

Русский

Униформная структура на E имеет базис, заданный по расстоянию: {p ∈ E×E | ‖p.fst / p.snd‖ < ε}.

LaTeX

$$$(\\mathcal{u} E).HasBasis (\\lambda \\varepsilon . 0 < \\varepsilon) (\\lambda \\varepsilon . \\{p : E \\times E \\mid \\|p.fst / p.snd\\| < \\varepsilon\\})$$$

Lean4

@[to_additive (attr := simp)]
theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]

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