Theorems · Definition · general topology

OpenPartialHomeomorph.univUnitBall

{E : Type u_1} → [inst : SeminormedAddCommGroup E] → [NormedSpace ℝ E] → OpenPartialHomeomorph E E

Local homeomorphism between a real (semi)normed space and the unit ball. See also Homeomorph.unitBall.

Defined in

Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Cited by

13 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpace