Closed balls of a chart covering a compact set

An open partial homeomorphism φ : M → E into a pseudometric space pulls closed balls of E back to M through φ.symm. This file proves that a compact subset A of the source of φ is covered by finitely many such balls centred at points of A, all lying in the target of φ and pulling back into a given neighbourhood of A (OpenPartialHomeomorph.exists_finset_closedBall_cover). It also identifies the fibre of a map f over f x, inside a chart ball about x on which x is the only point over f x, with {x} (OpenPartialHomeomorph.preimage_singleton_inter_symm_image_ball_eq_singleton).

theorem OpenPartialHomeomorph.exists_finset_closedBall_cover {M : Type u_1} {E : Type u_2} [TopologicalSpace M] [PseudoMetricSpace E] (φ : OpenPartialHomeomorph M E) {A U : Set M} (hA : IsCompact A) (hAφ : A ⊆ φ.source) (hU : U ∈ nhdsSet A) : ∃ (t : Finset M) (r : M → ℝ), (∀ a ∈ t, a ∈ A ∧ 0 < r a ∧ Metric.closedBall (↑φ a) (r a) ⊆ φ.target ∧ ↑φ.symm '' Metric.closedBall (↑φ a) (r a) ⊆ U) ∧ A ⊆ ↑φ.symm '' ⋃ a ∈ t, Metric.closedBall (↑φ a) (r a)

A compact subset A of the source of a chart φ is covered by finitely many closed balls of φ, centred at points of A, whose images lie in a given neighbourhood U of A.

theorem OpenPartialHomeomorph.preimage_singleton_inter_symm_image_ball_eq_singleton {M : Type u_1} {E : Type u_2} [TopologicalSpace M] [PseudoMetricSpace E] {N : Type u_3} {f : M → N} {x : M} (e : OpenPartialHomeomorph M E) (hx : x ∈ e.source) {r : ℝ} (hr : 0 < r) (hisol : ∀ z ∈ Metric.ball (↑e x) r, z ≠ ↑e x → f (↑e.symm z) ≠ f x) : f ⁻¹' {f x} ∩ ↑e.symm '' Metric.ball (↑e x) r = {x}

The fibre of f over f x inside a chart ball about x on which x is the only point over f x is {x}.