Zulip Chat Archive

Stream: maths

Topic: eq_zero_of_norm_lt

Johan Commelin (Mar 12 2021 at 08:21):

Do we know that x = 0 if the norm of x is < eps for all positive epsilon?

Heather Macbeth (Mar 12 2021 at 08:25):

Yup, docs#le_of_forall_pos_le_add

Heather Macbeth (Mar 12 2021 at 08:26):

(Well, that's for x itself rather than the norm of x.)

Heather Macbeth (Mar 12 2021 at 08:27):

Combine with docs#norm_eq_zero I suppose.

Sebastien Gouezel (Mar 12 2021 at 08:42):

or docs#norm_le_zero_iff

Johan Commelin (Mar 12 2021 at 08:42):

Thanks for the help!

Last updated: May 02 2025 at 03:31 UTC