Zulip Chat Archive

Stream: maths

Topic: eq_zero_of_norm_lt


view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Mar 12 2021 at 08:25):

Yup, docs#le_of_forall_pos_le_add

view this post on Zulip Heather Macbeth (Mar 12 2021 at 08:26):

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

view this post on Zulip Heather Macbeth (Mar 12 2021 at 08:27):

Combine with docs#norm_eq_zero I suppose.

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 08:42):

or docs#norm_le_zero_iff

view this post on Zulip Johan Commelin (Mar 12 2021 at 08:42):

Thanks for the help!


Last updated: May 14 2021 at 18:28 UTC