Zero of really small

Stream: maths

[Patrick Massot]

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

[Chris Hughes]

I think something like eq_of_forall_abs_sub_lt is in there.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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)

[Patrick Massot]

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

[Patrick Massot]

with weaker assumptions of course

[Patrick Massot]

(I mean replacing real numbers with something more general)

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

of course we could also prove them the other way around