Spheres and open subsets of closed balls

On a sphere of nonzero radius in a torsion-free seminormed additive group, a point and its antipode are distinct. Their complements therefore cover the sphere. This cover is useful for decomposing spheres into punctured spheres. Two points of a sphere centred at zero that are not antipodal have nonzero sum (TauCeti.coe_add_coe_ne_zero).

An open subset of a closed ball contained in the corresponding open ball embeds openly into the ambient space.

A map lifting every vector of norm less than r to a vector of norm less than r lifts each y to a vector of norm less than ‖y‖ + ε (TauCeti.exists_apply_eq_norm_lt_add).

Under an injective map, the image of v lies outside the image of the closed ball of radius r centred at zero exactly when r < ‖v‖ (Function.Injective.apply_notMem_image_closedBall_zero_iff).

A bijection of the closed unit ball preserving the unit sphere restricts to a bijection of the unit sphere (Equiv.restrictUnitSphere).

theorem TauCeti.compl_singleton_union_compl_singleton_neg {E : Type u_1} [SeminormedAddCommGroup E] [IsAddTorsionFree E] {r : ℝ} (hr : r ≠ 0) (p : ↑(Metric.sphere 0 r)) : {p}ᶜ ∪ {-p}ᶜ = Set.univ

The complements of two antipodal points cover any sphere of nonzero radius in a torsion-free seminormed additive group.

theorem TauCeti.coe_add_coe_ne_zero {E : Type u_1} [SeminormedAddCommGroup E] {r : ℝ} {b y : ↑(Metric.sphere 0 r)} (h : y ≠ -b) : ↑b + ↑y ≠ 0

Two points of a sphere centred at zero that are not antipodal have nonzero sum.

theorem IsOpen.isOpenEmbedding_coe_openSubset_closedBall {E : Type u_1} [SeminormedAddCommGroup E] {r : ℝ} {U : Set ↑(Metric.closedBall 0 r)} (hU : IsOpen U) (h : ∀ z ∈ U, ‖↑z‖ < r) : Topology.IsOpenEmbedding fun (z : ↑U) => ↑↑z

An open subset of a closed ball centered at zero whose points have norm strictly less than the radius embeds openly into the ambient space.

theorem TauCeti.exists_apply_eq_norm_lt_add {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} (hf : ∀ (r : ℝ), Metric.ball 0 r ⊆ f '' Metric.ball 0 r) (y : F) {ε : ℝ} (hε : 0 < ε) : ∃ (x : E), f x = y ∧ ‖x‖ < ‖y‖ + ε

If f lifts every vector of norm less than r to a vector of norm less than r, then every y is f x for some x with ‖x‖ < ‖y‖ + ε, for each ε > 0.

theorem Function.Injective.apply_notMem_image_closedBall_zero_iff {E : Type u_1} {X : Type u_2} [SeminormedAddGroup E] {e : E → X} (he : Injective e) {r : ℝ} {v : E} : e v ∉ e '' Metric.closedBall 0 r ↔ r < ‖v‖

Under an injective map e, the image of v lies outside the image of the closed ball of radius r centred at zero exactly when r < ‖v‖.

Bijections of the closed ball preserving the unit sphere

theorem Equiv.norm_symm_apply_eq_one_iff {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) (x : ↑(Metric.closedBall 0 1)) : ‖↑(D.symm x)‖ = 1 ↔ ‖↑x‖ = 1

If a bijection of the closed unit ball preserves the unit sphere, so does its inverse.

def Equiv.restrictUnitSphere {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) : ↑(Metric.sphere 0 1) ≃ ↑(Metric.sphere 0 1)

A bijection of the closed unit ball which preserves the unit sphere restricts to a bijection of the unit sphere.

@[simp]

theorem Equiv.coe_restrictUnitSphere_apply {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) (z : ↑(Metric.sphere 0 1)) : ↑((D.restrictUnitSphere hD) z) = ↑(D (Set.inclusion ⋯ z))

@[simp]

theorem Equiv.coe_restrictUnitSphere_symm_apply {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) (z : ↑(Metric.sphere 0 1)) : ↑((D.restrictUnitSphere hD).symm z) = ↑(D.symm (Set.inclusion ⋯ z))

theorem Equiv.inclusion_restrictUnitSphere_symm_apply {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) (z : ↑(Metric.sphere 0 1)) : Set.inclusion ⋯ ((D.restrictUnitSphere hD).symm z) = D.symm (Set.inclusion ⋯ z)

The inverse of D on the unit sphere, read in the closed unit ball.

theorem Equiv.apply_restrictUnitSphere_symm {V : Type u_1} [SeminormedAddCommGroup V] (D : ↑(Metric.closedBall 0 1) ≃ ↑(Metric.closedBall 0 1)) (hD : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑(D x)‖ = 1 ↔ ‖↑x‖ = 1) {σ : ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)} (hσ : ∀ (z : ↑(Metric.sphere 0 1)), D (Set.inclusion ⋯ z) = Set.inclusion ⋯ (σ z)) (z : ↑(Metric.sphere 0 1)) : σ ((D.restrictUnitSphere hD).symm z) = z

If D is σ on the unit sphere, then σ undoes the restriction of the inverse of D.