OpenMapping

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

Statistics

Metric	Count
Definitions	0
Theorems eventually_constant_or_nhds_le_map_nhds, eventually_constant_or_nhds_le_map_nhds_aux, eq_const_add_im_mul_I_of_re_eq_const, eq_const_of_im_eq_const, eq_const_of_re_eq_const, eq_re_add_const_mul_I_of_re_eq_const, is_constant_or_isOpen, is_constant_or_isOpenMap, isOpenQuotientMap_pow, isOpenQuotientMap_pow_compl_zero, isOpenQuotientMap_zpow_compl_zero, ball_subset_image_closedBall, C_eq_or_isOpenQuotientMap_eval, isOpenQuotientMap_eval	14
Total	14

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_constant_or_nhds_le_map_nhds 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Filter.Eventually nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.map	—	Metric.isOpen_iff isOpen_analyticAt Complex.instCompleteSpace comp dist_self_add_left norm_smul NormedSpace.toNormSMulClass mem_sphere_zero_iff_norm mul_one dist_zero_right add analyticAt_const ContinuousLinearMap.analyticAt IsScalarTower.left IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.eventually_of_mem Metric.ball_mem_nhds eq_or_ne Convex.isPreconnected IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing convex_ball sub_zero norm_inv norm_norm inv_mul_cancel₀ AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const Metric.mem_ball_self zero_smul add_zero dist_eq_norm Metric.mem_ball Complex.norm_real smul_smul mul_inv_cancel₀ one_smul add_sub_cancel eventually_constant_or_nhds_le_map_nhds_aux LE.le.trans Filter.map_compose Filter.map_mono Continuous.fun_add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_const Continuous.smul continuous_id' Continuous.tendsto
eventually_constant_or_nhds_le_map_nhds_aux 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Filter.Eventually nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.map	—	Filter.HasBasis.le_basis_iff Metric.nhds_basis_ball Filter.HasBasis.map Metric.nhds_basis_closedBall eventually_eq_or_eventually_ne analyticAt_const IsOpen.eventually_mem isOpen_analyticAt Complex.instCompleteSpace Filter.HasBasis.mem_iff Filter.Eventually.and eventually_nhdsWithin_iff DifferentiableOn.mono AnalyticOnNhd.differentiableOn Metric.ball_subset_closedBall AnalyticOnNhd.continuousOn closure_ball LT.lt.ne GT.gt.lt lt_inf_iff Metric.closedBall_subset_closedBall inf_le_left DiffContOnCl.mono Metric.ball_subset_ball Metric.sphere_subset_closedBall Metric.ne_of_mem_sphere NormedSpace.sphere_nonempty EMetric.instNontrivialTopologyOfNontrivial Complex.instNontrivial LT.lt.le Continuous.comp_continuousOn continuous_norm ContinuousOn.mono DiffContOnCl.continuousOn_ball DiffContOnCl.sub_const IsCompact.exists_isMinOn instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid isCompact_sphere Complex.instProperSpace Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_sub_pos_iff HasSubset.Subset.trans Set.instIsTransSubset DiffContOnCl.ball_subset_image_closedBall Filter.not_eventually Set.image_mono inf_le_right

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_const_add_im_mul_I_of_re_eq_const 📖	mathematical	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.im IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsConnected	Complex.instAdd Complex.ofReal Complex.instMul Complex.I	—	eq_const_of_im_eq_const MulZeroClass.mul_zero mul_one sub_self add_zero zero_add
eq_const_of_im_eq_const 📖	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.im IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsConnected	—	—	IsConnected.nonempty
eq_const_of_re_eq_const 📖	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.re IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsConnected	—	—	IsConnected.nonempty
eq_re_add_const_mul_I_of_re_eq_const 📖	mathematical	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.re IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsConnected	Complex.instAdd Complex.ofReal Complex.instMul Complex.I	—	eq_const_of_re_eq_const MulZeroClass.mul_zero mul_one sub_self add_zero zero_add
is_constant_or_isOpen 📖	mathematical	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	IsOpen SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.image	—	eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const isOpen_iff_mem_nhds AnalyticAt.eventually_constant_or_nhds_le_map_nhds Filter.image_mem_map IsOpen.mem_nhds
is_constant_or_isOpenMap 📖	mathematical	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.univ	IsOpenMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	Set.subset_univ is_constant_or_isOpen PreconnectedSpace.isPreconnected_univ ConnectedSpace.toPreconnectedSpace PathConnectedSpace.connectedSpace NormedSpace.instPathConnectedSpace

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenQuotientMap_pow 📖	mathematical	—	IsOpenQuotientMap Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Polynomial.eval_pow Polynomial.eval_X Polynomial.isOpenQuotientMap_eval Polynomial.natDegree_pow NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Polynomial.natDegree_X instNontrivial mul_one
isOpenQuotientMap_pow_compl_zero 📖	mathematical	—	IsOpenQuotientMap Complex instZero instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedCommRing.toNormedRing NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing	—	pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsOpenQuotientMap.surjective isOpenQuotientMap_pow zero_pow Continuous.comp' Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' continuous_subtype_val Topology.IsOpenEmbedding.isOpenMap_iff IsOpen.isOpenEmbedding_subtypeVal IsClosed.isOpen_compl isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsOpenMap.comp IsOpenQuotientMap.isOpenMap IsOpen.isOpenMap_subtype_val
isOpenQuotientMap_zpow_compl_zero 📖	mathematical	—	IsOpenQuotientMap Complex instZero instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DivInvMonoid.toZPow instDivInvMonoid zpow_ne_zero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instField	—	zpow_ne_zero Nat.cast_ne_zero Int.instCharZero isOpenQuotientMap_pow_compl_zero neg_ne_zero pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing zpow_neg zpow_natCast inv_pow IsOpenQuotientMap.comp Homeomorph.isOpenQuotientMap

DiffContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_subset_image_closedBall 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.instLT Real.instZero Real.instLE Norm.norm Complex.instNorm Complex.instSub Filter.Frequently nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set Set.instHasSubset DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Set.image Metric.closedBall	—	Nat.instAtLeastTwoHAddOfNat sub_const Continuous.comp_continuousOn continuous_norm continuousOn closure_ball LT.lt.ne DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn Metric.isOpen_ball le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Metric.mem_ball norm_sub_sub_norm_sub_le_norm_sub dist_comm Metric.exists_isLocalMin_mem_ball Complex.instProperSpace instOrderTopologyReal Metric.mem_closedBall_self LT.lt.le LT.lt.trans_le Metric.ball_subset_closedBall sub_eq_zero DifferentiableOn.eventually_differentiableAt IsOpen.mem_nhds Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm Filter.mp_mem Filter.univ_mem' Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace Filter.Eventually.filter_mono nhdsWithin_le_nhds Convex.isPreconnected IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const Metric.mem_ball_self Filter.not_eventually Filter.mem_of_superset Metric.ball_mem_nhds

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_eq_or_isOpenQuotientMap_eval 📖	mathematical	—	DFunLike.coe RingHom Complex Polynomial Complex.instSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C IsOpenQuotientMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField eval	—	AnalyticOnNhd.is_constant_or_isOpenMap AnalyticOnNhd.eval_polynomial funext instIsDomain IsAlgClosed.instInfinite Complex.isAlgClosed eval_C IsAlgClosed.eval_surjective Iff.not natDegree_eq_zero continuous_aeval IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
isOpenQuotientMap_eval 📖	mathematical	—	IsOpenQuotientMap Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField eval Complex.instSemiring	—	C_eq_or_isOpenQuotientMap_eval Iff.not natDegree_eq_zero

---

← Back to Index