Closed subsets of closed subspaces

Stream: new members

[Joseph Cooper]

import Mathlib

example: @IsClosed (↥(Metric.closedBall (0:ℂ) 2)) instTopologicalSpaceSubtype ({z| ↑z ∈ Metric.closedBall (0:ℂ) (1)}):= by
  sorry

In order to prove this statement, is there a lemma in Mathlib similar to this?
Or is there an alternative approach to this problem, that may be easier, given lemmas/theorems in Mathlib?

[Yaël Dillies]

docs#isClosed_ball ?

[Joseph Cooper]

Yaël Dillies said:

docs#isClosed_ball ?

Applying Metric.isClosed_ball results in "busily processing" for a long time. Do results like this figure out the context of the subspace topology?

[Jireh Loreaux]

Did you get the Mathlib cache?

[Jireh Loreaux]

oh, I see, you're working with the subtype.

[Luigi Massacci]

Can I ask what you want to do? (the statement is not very natural in Lean) This seems like an #xy problem kind of situation

[Luigi Massacci]

Though here is a bad proof if you care for it:

example: @IsClosed (Metric.closedBall (0:ℂ) 2) instTopologicalSpaceSubtype ({z| ↑z ∈ Metric.closedBall (0:ℂ) (1)}):= by
  simp only [Metric.mem_closedBall, dist_zero_right, Complex.norm_eq_abs]
  exact isClosed_le (Continuous.comp Complex.continuous_abs continuous_subtype_val) continuous_const