Zulip Chat Archive

Stream: maths

Topic: Zero of really small


view this post on Zulip Patrick Massot (Jan 19 2019 at 21:44):

Where do we find lemma zero_of_abs_lt_all (x : ℝ) (h : ∀ ε, ε > 0 → |x| < ε) : x = 0?

view this post on Zulip Chris Hughes (Jan 19 2019 at 21:48):

I think something like eq_of_forall_abs_sub_lt is in there.

view this post on Zulip Patrick Massot (Jan 19 2019 at 21:54):

https://github.com/leanprover/mathlib/search?q=eq_of_forall_abs_sub_lt&unscoped_q=eq_of_forall_abs_sub_lt :sad:

view this post on Zulip Patrick Massot (Jan 19 2019 at 21:54):

Do you have any idea where something like this could be?

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:14):

lemma zero_of_abs_lt_all (x : ) (h :  ε, ε > 0  |x| < ε) : x = 0 :=
eq_zero_of_abs_eq_zero $ eq_of_le_of_forall_le_of_dense (abs_nonneg x) $ λ ε ε_pos, le_of_lt (h ε ε_pos)

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:15):

@Mario Carneiro Should I PR that, or is it already in?

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:16):

with weaker assumptions of course

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:17):

(I mean replacing real numbers with something more general)

view this post on Zulip Mario Carneiro (Jan 19 2019 at 22:23):

is this a theorem of normed groups or do you want a different abstraction

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:24):

I think normed groups is enough for me, but eq_of_le_of_forall_le_of_dense has more exotic type classes

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:26):

But I don't want you to think too hard about this when you could be hitting that merge button on https://github.com/leanprover/mathlib/pull/610

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:31):

lemma zero_of_norm_lt_all {G : Type*} [normed_group G] (x : G) (h :  ε, ε > 0  x < ε) : x = 0 :=
(norm_eq_zero _).1 $ eq_of_le_of_forall_le_of_dense (norm_nonneg x) $ λ ε ε_pos, le_of_lt (h ε ε_pos)

lemma zero_of_abs_lt_all (x : ) (h :  ε, ε > 0  |x| < ε) : x = 0 :=
zero_of_norm_lt_all x h

does work

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:31):

of course we could also prove them the other way around


Last updated: May 14 2021 at 20:13 UTC