AbsMax

📁 Source: Mathlib/Analysis/Complex/AbsMax.lean

Statistics

Metric	Count
Definitions	0
Theorems eqOn_closedBall_of_isMaxOn_norm, eqOn_closure_of_eqOn_frontier, eqOn_closure_of_isPreconnected_of_isMaxOn_norm, eqOn_of_eqOn_frontier, eqOn_of_isPreconnected_of_isMaxOn_norm, eq_const_of_exists_le, eq_const_of_exists_max, eq_of_isMaxOn_of_ball_subset, eventually_eq_of_isLocalMax_norm, eventually_eq_or_eq_zero_of_isLocalMin_norm, exists_mem_frontier_isMaxOn_norm, isOpen_setOf_mem_nhds_and_isMaxOn_norm, norm_eqOn_closedBall_of_isMaxOn, norm_eqOn_closure_of_isPreconnected_of_isMaxOn, norm_eqOn_of_isPreconnected_of_isMaxOn, norm_eq_norm_of_isMaxOn_of_ball_subset, norm_eventually_eq_of_isLocalMax, norm_le_of_forall_mem_frontier_norm_le, norm_max_aux₁, norm_max_aux₂, norm_max_aux₃	21
Total	21

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_closedBall_of_isMaxOn_norm 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	eq_of_isMaxOn_of_ball_subset Metric.ball_subset_ball
eqOn_closure_of_eqOn_frontier 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set.EqOn frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set.EqOn closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	norm_le_of_forall_mem_frontier_norm_le DiffContOnCl.sub sub_self norm_zero instReflLe
eqOn_closure_of_isPreconnected_of_isMaxOn_norm 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Set.EqOn.of_subset_closure TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace eqOn_of_isPreconnected_of_isMaxOn_norm DiffContOnCl.differentiableOn DiffContOnCl.continuousOn continuousOn_const subset_closure Set.Subset.rfl
eqOn_of_eqOn_frontier 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set.EqOn frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set.EqOn	—	Set.EqOn.mono subset_closure eqOn_closure_of_eqOn_frontier
eqOn_of_isPreconnected_of_isMaxOn_norm 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	norm_eqOn_of_isPreconnected_of_isMaxOn DifferentiableOn.add_const IsMaxOn.norm_add_self eq_of_norm_eq_of_norm_add_eq SameRay.norm_add SameRay.rfl Real.instIsStrictOrderedRing
eq_const_of_exists_le 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instLE Real.instZero Real.instLT Set Set.instMembership Metric.closedBall Norm.norm NormedAddCommGroup.toNorm	Set.EqOn NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ProperSpace.isCompact_closedBall Metric.nonempty_closedBall ContinuousOn.norm ContinuousOn.mono DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Metric.closedBall_subset_ball eq_const_of_exists_max LE.le.trans Metric.mem_ball_self LE.le.trans_lt
eq_const_of_exists_max 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	eqOn_of_isPreconnected_of_isMaxOn_norm Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball Metric.isOpen_ball
eq_of_isMaxOn_of_ball_subset 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Dist.dist PseudoMetricSpace.toDist	—	—	norm_eq_norm_of_isMaxOn_of_ball_subset DiffContOnCl.add_const IsMaxOn.norm_add_self eq_of_norm_eq_of_norm_add_eq SameRay.norm_add SameRay.rfl Real.instIsStrictOrderedRing
eventually_eq_of_isLocalMax_norm 📖	mathematical	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds IsLocalMax Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Filter.Eventually nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Filter.HasBasis.eventually_iff Metric.nhds_basis_closedBall Filter.Eventually.and eqOn_closedBall_of_isMaxOn_norm DifferentiableOn.diffContOnCl DifferentiableAt.differentiableWithinAt Metric.closure_ball_subset_closedBall Metric.ball_subset_closedBall
eventually_eq_or_eq_zero_of_isLocalMin_norm 📖	mathematical	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace addCommGroup instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing nhds IsLocalMin Real Real.instPreorder Norm.norm instNorm	Filter.Eventually Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instZero	—	ContinuousAt.eventually_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace DifferentiableAt.continuousAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Filter.Eventually.self_of_nhds IsLocalMin.inv Real.instIsStrictOrderedRing Filter.Eventually.mono norm_pos_iff IsLocalMax.congr Filter.Eventually.of_forall norm_inv Filter.mp_mem Filter.univ_mem' DifferentiableAt.inv eventually_eq_of_isLocalMax_norm UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace
exists_mem_frontier_isMaxOn_norm 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Nonempty DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField	Set Set.instMembership frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm closure	—	Bornology.IsBounded.isCompact_closure FiniteDimensional.proper_real Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.complexToReal Module.Projective.of_free Module.Free.of_divisionRing IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.Nonempty.closure ContinuousOn.norm DiffContOnCl.continuousOn Set.mem_union closure_eq_interior_union_frontier ne_top_of_le_ne_top IsCompact.ne_univ RealNormedSpace.noncompactSpace interior_subset_closure exists_mem_frontier_infDist_compl_eq_dist frontier_interior_subset LE.le.trans_eq Membership.mem.out norm_eq_norm_of_isMaxOn_of_ball_subset IsMaxOn.on_subset subset_closure dist_comm HasSubset.Subset.trans Set.instIsTransSubset Metric.ball_infDist_compl_subset interior_subset
isOpen_setOf_mem_nhds_and_isMaxOn_norm 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup setOf Set Filter Filter.instMembership nhds IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	isOpen_iff_mem_nhds Filter.Eventually.and eventually_eventually_nhds DifferentiableOn.eventually_differentiableAt Filter.Eventually.mono norm_eventually_eq_of_isLocalMax IsMaxOn.isLocalMax le_trans Membership.mem.out Eq.ge
norm_eqOn_closedBall_of_isMaxOn 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Real Norm.norm NormedAddCommGroup.toNorm Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	eq_or_ne dist_comm Metric.mem_closedBall Differentiable.add_const Differentiable.smul_const NormedSpace.toIsBoundedSMul IsScalarTower.left differentiable_id dist_zero_right CStarRing.norm_of_mem_unitary RCLike.instCStarRing instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass Set.MapsTo.mono LipschitzWith.mapsTo_ball lipschitzWith_lineMap nndist_eq_zero Set.Subset.rfl AffineMap.lineMap_apply_zero mul_one Metric.ball_subset_ball norm_max_aux₃ DiffContOnCl.comp Differentiable.diffContOnCl IsMaxOn.comp_mapsTo AffineMap.lineMap_apply_one
norm_eqOn_closure_of_isPreconnected_of_isMaxOn 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Real Norm.norm NormedAddCommGroup.toNorm closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Set.EqOn.of_subset_closure TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace norm_eqOn_of_isPreconnected_of_isMaxOn DiffContOnCl.differentiableOn ContinuousOn.norm DiffContOnCl.continuousOn continuousOn_const subset_closure Set.Subset.rfl
norm_eqOn_of_isPreconnected_of_isMaxOn 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Real Norm.norm NormedAddCommGroup.toNorm	—	le_antisymm IsOpen.mem_nhds_iff isOpen_setOf_mem_nhds_and_isMaxOn_norm ContinuousOn.isOpen_inter_preimage ContinuousOn.norm DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul isOpen_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Set.disjoint_left LE.le.trans_eq Membership.mem.out eq_or_ne IsPreconnected.subset_left_of_subset_union
norm_eq_norm_of_isMaxOn_of_ball_subset 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Dist.dist PseudoMetricSpace.toDist	Norm.norm NormedAddCommGroup.toNorm	—	norm_eqOn_closedBall_of_isMaxOn DiffContOnCl.mono IsMaxOn.on_subset Metric.mem_closedBall le_rfl
norm_eventually_eq_of_isLocalMax 📖	mathematical	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds IsLocalMax Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Filter.Eventually Real Norm.norm NormedAddCommGroup.toNorm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Filter.HasBasis.eventually_iff Metric.nhds_basis_closedBall Filter.Eventually.and norm_eqOn_closedBall_of_isMaxOn DifferentiableOn.diffContOnCl DifferentiableAt.differentiableWithinAt Metric.closure_ball_subset_closedBall Metric.ball_subset_closedBall
norm_le_of_forall_mem_frontier_norm_le 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm	—	Set.mem_union Set.union_comm closure_eq_self_union_frontier exists_ne Differentiable.add_const Differentiable.smul_const NormedSpace.toIsBoundedSMul IsScalarTower.left differentiable_id antilipschitzWith_lineMap DiffContOnCl.comp Differentiable.diffContOnCl Set.mapsTo_preimage AffineMap.lineMap_apply_zero exists_mem_frontier_isMaxOn_norm instNontrivial Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self AntilipschitzWith.isBounded_preimage subset_closure Continuous.frontier_preimage_subset Differentiable.continuous IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul
norm_max_aux₁ 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Dist.dist PseudoMetricSpace.toDist IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Metric.closedBall	Norm.norm NormedAddCommGroup.toNorm	—	Metric.mem_closedBall le_rfl LE.le.antisymm isMaxOn_iff not_lt dist_pos LT.lt.ne Nat.instAtLeastTwoHAddOfNat Metric.sphere_subset_closedBall circleIntegral.norm_integral_lt_of_norm_le_const_of_lt ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn_id continuousOn_const sub_ne_zero Metric.ne_of_mem_sphere LT.lt.ne' ContinuousOn.mono DiffContOnCl.continuousOn_ball le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_smul NormedSpace.toNormSMulClass norm_inv mem_sphere_iff_norm mul_comm mul_inv_cancel_left₀ div_eq_inv_mul dist_eq_norm div_lt_div_iff_of_pos_right mul_div_cancel₀ mul_assoc DiffContOnCl.circleIntegral_sub_inv_smul Metric.mem_ball_self norm_mul norm_ofNat norm_real norm_I mul_one IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain IsCancelMulZero.toIsLeftCancelMulZero Real.instIsOrderedAddMonoid LT.lt.le Real.pi_pos RCLike.charZero_rclike
norm_max_aux₂ 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Dist.dist PseudoMetricSpace.toDist IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Metric.closedBall	Norm.norm NormedAddCommGroup.toNorm	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformSpace.Completion.norm_coe norm_max_aux₁ UniformSpace.Completion.completeSpace Differentiable.comp_diffContOnCl ContinuousLinearMap.differentiable
norm_max_aux₃ 📖	mathematical	Dist.dist Complex PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DiffContOnCl DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Norm.norm NormedAddCommGroup.toNorm	—	eq_or_ne norm_max_aux₂ IsMaxOn.closure HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.norm DiffContOnCl.continuousOn closure_ball dist_ne_zero

---

← Back to Index