FiniteDimensional

📁 Source: Mathlib/Analysis/Calculus/InverseFunctionTheorem/FiniteDimensional.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_homeomorph_extension	1
Total	1

ApproximatesLinearOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_homeomorph_extension 📖	mathematical	ApproximatesLinearOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearEquiv.toContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringNNReal lipschitzExtensionConstant NNReal.instInv NNNorm.nnnorm ContinuousLinearMap SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearEquiv.symm	Set.EqOn DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	RingHomInvPair.ids RingHomIsometric.ids LipschitzOnWith.extend_finite_dimension lipschitzOnWith add_sub_cancel LipschitzOnWith.approximatesLinearOn lipschitzOnWith_univ add_sub_cancel_left complete_of_proper FiniteDimensional.proper_real LinearEquiv.finiteDimensional

---

← Back to Index