## Stream: maths

### Topic: Zero of really small

#### Patrick Massot (Jan 19 2019 at 21:44):

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

#### Chris Hughes (Jan 19 2019 at 21:48):

I think something like eq_of_forall_abs_sub_lt is in there.

#### Patrick Massot (Jan 19 2019 at 21:54):

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

#### 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)


#### Patrick Massot (Jan 19 2019 at 22:15):

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

#### Patrick Massot (Jan 19 2019 at 22:16):

with weaker assumptions of course

#### Patrick Massot (Jan 19 2019 at 22:17):

(I mean replacing real numbers with something more general)

#### Mario Carneiro (Jan 19 2019 at 22:23):

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

#### 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

#### 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

#### 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

#### 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