Theorems · Definition · general topology

OpenPartialHomeomorph.univBall

{E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      {P : Type u_2} → [inst_2 : PseudoMetricSpace P] → [NormedAddTorsor E P] → P → ℝ → OpenPartialHomeomorph E P

If r > 0, then OpenPartialHomeomorph.univBall c r is a smooth open partial homeomorphism with source = Set.univ and target = Metric.ball c r. Otherwise, it is the translation by c. Thus in all cases, it sends 0 to c, see OpenPartialHomeomorph.univBall_apply_zero.

Defined in

Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Cited by

9 results in Mathlib

Foundations

Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsor