Complex

📁 Source: Mathlib/Geometry/Manifold/Complex.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax, apply_eq_of_compactSpace, exists_eq_const_of_compactSpace, isLocallyConstant, apply_eq_of_isPreconnected_isCompact_isOpen, eqOn_of_isPreconnected_of_isMaxOn_norm, norm_eqOn_of_isPreconnected_of_isMaxOn	7
Total	7

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax 📖	—	Filter.Eventually MDifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf nhds IsLocalMax Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	—	ModelWithCorners.Boundaryless.range_eq_univ nhdsWithin_univ map_extChartAt_symm_nhdsWithin_range Filter.eventually_map extChartAt_target_mem_nhdsWithin Filter.mp_mem Filter.Tendsto.eventually Eq.le Filter.univ_mem' extChartAt_source PartialEquiv.map_target Set.mem_univ PartialEquiv.right_inv differentiableWithinAt_univ mdifferentiableAt_iff_of_mem_source IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace extChartAt_to_inv norm_eventually_eq_of_isLocalMax

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_of_compactSpace 📖	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	—	—	IsLocallyConstant.apply_eq_of_preconnectedSpace isLocallyConstant
exists_eq_const_of_compactSpace 📖	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	—	—	IsLocallyConstant.exists_eq_const AddTorsor.nonempty isLocallyConstant
isLocallyConstant 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	IsLocallyConstant	—	IsLocallyConstant.of_constant_on_preconnected_clopens ChartedSpace.locallyConnectedSpace Homeomorph.locallyConnectedSpace instLocallyConnectedSpace LocallyConvexSpace.toLocPathConnectedSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul NormedSpace.toLocallyConvexSpace MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen mdifferentiableOn IsClosed.isCompact IsClopen.isClosed IsClopen.isOpen

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_of_isPreconnected_isCompact_isOpen 📖	—	MDifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf IsPreconnected IsCompact IsOpen Set Set.instMembership	—	—	IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.norm continuousOn norm_eqOn_of_isPreconnected_of_isMaxOn norm_eq_zero norm_zero ContinuousWithinAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup ChartedSpace.LiftPropWithinAt.continuousWithinAt continuousWithinAt_const DifferentiableWithinAt.sub_const ChartedSpace.LiftPropWithinAt.prop sub_self
eqOn_of_isPreconnected_of_isMaxOn_norm 📖	mathematical	MDifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf IsPreconnected IsOpen Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	norm_eqOn_of_isPreconnected_of_isMaxOn ContinuousWithinAt.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ChartedSpace.LiftPropWithinAt.continuousWithinAt continuousWithinAt_const DifferentiableWithinAt.add_const ChartedSpace.LiftPropWithinAt.prop IsMaxOn.norm_add_self eq_of_norm_eq_of_norm_add_eq SameRay.norm_add SameRay.rfl Real.instIsStrictOrderedRing
norm_eqOn_of_isPreconnected_of_isMaxOn 📖	mathematical	MDifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf IsPreconnected IsOpen Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	isOpen_iff_mem_nhds Filter.inter_mem IsOpen.mem_nhds Filter.mem_of_superset LE.le.trans_eq Membership.mem.out Filter.Eventually.mono eventually_mem_nhds_iff mdifferentiableAt Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax ContinuousOn.isOpen_inter_preimage ContinuousOn.norm continuousOn isOpen_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Disjoint.mono inf_le_right disjoint_compl_right eq_or_ne IsPreconnected.subset_left_of_subset_union

---

← Back to Index