NormedSpace

📁 Source: Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean

Statistics

Metric	Count
Definitions ConformalAt	1
Theorems comp, conformalAt, const_smul, differentiable, comp, const_smul, differentiableAt, conformalAt, conformalAt_const_smul, conformalAt_id, conformalAt_iff_isConformalMap_fderiv, conformal_const_smul, conformal_id	13
Total	14

Conformal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	Conformal	—	—	ConformalAt.comp
conformalAt 📖	mathematical	Conformal	ConformalAt	—	—
const_smul 📖	mathematical	Conformal	Real Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	ConformalAt.const_smul
differentiable 📖	mathematical	Conformal	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ConformalAt.differentiableAt

ConformalAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ConformalAt	—	—	RingHomCompTriple.ids HasFDerivAt.comp IsConformalMap.comp
const_smul 📖	mathematical	ConformalAt	Real Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	comp conformalAt_const_smul
differentiableAt 📖	mathematical	ConformalAt	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	HasFDerivAt.differentiableAt

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conformalAt 📖	mathematical	—	ConformalAt	—	hasFDerivAt_of_subsingleton isConformalMap_of_subsingleton

(root)

Definitions

Name	Category	Theorems
ConformalAt 📖	MathDef	9 math math: conformalAt_iff, conformalAt_id, conformalAt_const_smul, Conformal.conformalAt, conformalAt_iff_isConformalMap_fderiv, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, DifferentiableAt.conformalAt, conformalAt_iff', Subsingleton.conformalAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conformalAt_const_smul 📖	mathematical	—	ConformalAt Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivAt.const_smul hasFDerivAt_id isConformalMap_const_smul
conformalAt_id 📖	mathematical	—	ConformalAt	—	hasFDerivAt_id isConformalMap_id
conformalAt_iff_isConformalMap_fderiv 📖	mathematical	—	ConformalAt IsConformalMap Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup fderiv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace DifferentiableAt.hasFDerivAt Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim fderiv_zero_of_not_differentiableAt IsConformalMap.ne_zero
conformal_const_smul 📖	mathematical	—	Conformal Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	conformalAt_const_smul
conformal_id 📖	mathematical	—	Conformal	—	conformalAt_id

---

← Back to Index