Preimage of normed ball

Stream: Is there code for X?

[Moritz Doll]

Does this lemma already exist somewhere? I could not find it in normed_group and neither could library_search. If it does not exist what would be a good name?

import analysis.normed.group.basic

variables {𝕜 F : Type*}

variables [normed_group 𝕜]
variables (f : F → 𝕜)

lemma closed_ball_preimage (r : ℝ) : {y : F | ∥f y∥ ≤ r} =
  f ⁻¹' (metric.closed_ball (0 : 𝕜) r) :=
by { ext y, simp }

[Patrick Massot]

It seems very specialized to me, do you really need this very often?

[Eric Wieser]

That's basically true by refl besides the sub_zero, right?

[Eric Wieser]

Which direction do you think you need the lemma in? Currently the name is for the opposite direction to the statement

[Patrick Massot]

You also need to use the fact that the distance is given by the norm.

[Patrick Massot]

A direct proof would be: unfold set.preimage, simp_rw mem_closed_ball_zero_iff

[Moritz Doll]

I only need it once (for now), so I have to problem with using it inline. To avoid an xy-problem: I want to prove that {y : F | ∥f y∥ ≤ r} is closed (for continuous f).

[Kevin Buzzard]

This is just "closed balls are closed" plus "preimage of closed is closed"

[Moritz Doll]

Yes of course, but in Lean it needs some (trivial) rewrite first

[Anatole Dedecker]

I think you can avoid rewriting by using docs#continuous.norm and docs#is_closed_Iic, although it’s less mathematically satisfying

[Floris van Doorn]

Moritz Doll said:

I only need it once (for now), so I have to problem with using it inline. To avoid an xy-problem: I want to prove that {y : F | ∥f y∥ ≤ r} is closed (for continuous f).

If hf : continuous f, then this is is_closed_le hf.norm continuous_const.