Topology

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Statistics

Metric	Count
Definitions instTopologicalSpace, ofComplex, verticalStrip, «term↑ₕ_»	4
Theorems upperHalfPlaneMk, J_smul, ModularGroup_T_zpow_mem_verticalStrip, comp_ofComplex, comp_ofComplex_of_im_le_zero, comp_ofComplex_of_im_pos, continuous_coe, continuous_im, continuous_re, eventuallyEq_coe_comp_ofComplex, instContinuousGLSMul, instContractibleSpace, instLocPathConnectedSpace, instLocallyCompactSpace, instNoncompactSpace, instSecondCountableTopology, instT3Space, instT4Space, isEmbedding_coe, isOpenEmbedding_coe, isOpenMap_im, isOpenMap_norm, isOpenMap_re, mem_verticalStrip_iff, ofComplex_apply, ofComplex_apply_eq_ite, ofComplex_apply_eq_of_im_nonpos, ofComplex_apply_of_im_nonpos, ofComplex_apply_of_im_pos, subset_verticalStrip_of_isCompact, verticalStrip_anti_right, verticalStrip_mono, verticalStrip_mono_left	33
Total	37

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
upperHalfPlaneMk 📖	mathematical	Continuous Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.instLT Real.instZero Complex.im	Continuous UpperHalfPlane UpperHalfPlane.instTopologicalSpace	—	Topology.IsEmbedding.continuous_iff UpperHalfPlane.isEmbedding_coe

UpperHalfPlane

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	87 math math: mdifferentiable_num, CuspFormClass.holo, ModularFormClass.differentiableAt_comp_ofComplex, instContinuousSMulGL2R, CuspFormClass.zero_at_infty_comp_ofComplex, analyticAt_smul, isOpenEmbedding_coe, deriv_smul, comp_ofComplex_of_im_pos, isOpenMap_norm, isOpenMap_im, Continuous.upperHalfPlaneMk, comp_ofComplex, isOpenMap_re, mdifferentiable_inv_denom, ofComplex_apply_of_im_nonpos, ModularFormClass.continuous, contMDiff_coe, CuspForm.holo', instLocPathConnectedSpace, contMDiff_inv_denom, instT4Space, isProperMap_smul_I, instNoncompactSpace, ofComplex_apply_of_im_pos, instContractibleSpace, hasStrictDerivAt_smul, SlashInvariantFormClass.periodic_comp_ofComplex, contMDiff_num, mdifferentiable_denom, ModularGroup.fd_eq_closure_fdo, ofComplex_apply_eq_of_im_nonpos, instIsFiniteMeasureOnCompactsComapComplexCoeVolume, instProperSMul, MDifferentiable.slash, ofComplex_apply_eq_ite, petersson_continuous, J_smul, contMDiff_denom_zpow, ModularGroup.fdo_eq_interior_fd, ModularGroup.isOpen_fdo, ofComplex_apply, instLocallyCompactSpace, continuous_toSL2R, instIsLocallyFiniteMeasureVolume, IsZeroAtImInfty.zero_at_infty_comp_ofComplex, eventuallyEq_coe_comp_ofComplex, comp_ofComplex_of_im_le_zero, continuous_im, meromorphicOrderAt_comp_smul, Derivative.normalizedDerivOfComplex_mdifferentiable, instBorelSpace, instT3Space, mdifferentiable_jacobiTheta, contMDiffAt_ofComplex, ModularFormClass.bounded_at_infty_comp_ofComplex, ModularForm.holo', instSecondCountableTopology, contMDiffAt_iff, instIsManifoldComplexModelWithCornersSelfTopWithTopENat, instContinuousGLSMul, mdifferentiable_coe, EisensteinSeries.eisSummand_extension_differentiableOn, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, ModularFormClass.holo, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, mdifferentiableAt_iff, instContinuousSMulSL2R, contMDiff_smul, tendsto_comap_im_ofComplex, contMDiff_denom, E2_mdifferentiable, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, mdifferentiable_denom_zpow, instIsLocallyFiniteMeasureComapComplexCoeVolume, continuous_coe, Derivative.serreDerivative_mdifferentiable, hasStrictFDerivAt_smul, mdifferentiable_iff, isEmbedding_coe, instIsFiniteMeasureOnCompactsVolume, mdifferentiableAt_ofComplex, ModularGroup.isClosed_fd, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, mdifferentiable_smul, ModularGroup.isCompact_truncatedFundamentalDomain, continuous_re
ofComplex 📖	CompOp	28 math math: ModularFormClass.differentiableAt_comp_ofComplex, CuspFormClass.zero_at_infty_comp_ofComplex, analyticAt_smul, deriv_smul, comp_ofComplex_of_im_pos, comp_ofComplex, ofComplex_apply_of_im_nonpos, ofComplex_apply_of_im_pos, hasStrictDerivAt_smul, SlashInvariantFormClass.periodic_comp_ofComplex, ofComplex_apply_eq_of_im_nonpos, ofComplex_apply_eq_ite, J_smul, ofComplex_apply, IsZeroAtImInfty.zero_at_infty_comp_ofComplex, eventuallyEq_coe_comp_ofComplex, comp_ofComplex_of_im_le_zero, meromorphicOrderAt_comp_smul, contMDiffAt_ofComplex, ModularFormClass.bounded_at_infty_comp_ofComplex, contMDiffAt_iff, EisensteinSeries.eisSummand_extension_differentiableOn, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, mdifferentiableAt_iff, tendsto_comap_im_ofComplex, hasStrictFDerivAt_smul, mdifferentiable_iff, mdifferentiableAt_ofComplex
verticalStrip 📖	CompOp	6 math math: subset_verticalStrip_of_isCompact, ModularGroup_T_zpow_mem_verticalStrip, verticalStrip_anti_right, verticalStrip_mono, mem_verticalStrip_iff, verticalStrip_mono_left
«term↑ₕ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
J_smul 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction J OpenPartialHomeomorph.toFun' Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex Complex.instNeg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing coe	—	ext coe_J_smul neg_neg im_pos ofComplex_apply_of_im_pos
ModularGroup_T_zpow_mem_verticalStrip 📖	mathematical	—	UpperHalfPlane Set Set.instMembership verticalStrip Real Real.instNatCast im Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Ring.toIntAlgebra Real.instRing DivInvMonoid.toZPow Group.toDivInvMonoid Matrix.SpecialLinearGroup.instGroup ModularGroup.T	—	modular_T_zpow_smul mul_neg neg_mul Int.cast_natCast add_comm Int.cast_neg Int.cast_mul Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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.sub_congr Mathlib.Tactic.Ring.sub_pf abs_eq_self Int.sub_floor_div_mul_nonneg Real.instIsStrictOrderedRing LT.lt.le Int.sub_floor_div_mul_lt vadd_im instReflLe
comp_ofComplex 📖	mathematical	—	Complex UpperHalfPlane OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex coe	—	ofComplex_apply
comp_ofComplex_of_im_le_zero 📖	mathematical	Real Real.instLE Complex.im Real.instZero	Complex UpperHalfPlane OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex	—	ofComplex_apply_of_im_nonpos
comp_ofComplex_of_im_pos 📖	mathematical	Real Real.instLT Real.instZero Complex.im	Complex UpperHalfPlane OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex	—	ofComplex_apply
continuous_coe 📖	mathematical	—	Continuous UpperHalfPlane Complex instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField coe	—	Topology.IsEmbedding.continuous isEmbedding_coe
continuous_im 📖	mathematical	—	Continuous UpperHalfPlane Real instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace im	—	Continuous.comp Complex.continuous_im continuous_coe
continuous_re 📖	mathematical	—	Continuous UpperHalfPlane Real instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace re	—	Continuous.comp Complex.continuous_re continuous_coe
eventuallyEq_coe_comp_ofComplex 📖	mathematical	Real Real.instLT Real.instZero Complex.im	Filter.EventuallyEq Complex nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField UpperHalfPlane coe OpenPartialHomeomorph.toFun' instTopologicalSpace ofComplex	—	Filter.mp_mem IsOpen.mem_nhds isOpen_upperHalfPlaneSet Filter.univ_mem' ofComplex_apply_of_im_pos
instContinuousGLSMul 📖	mathematical	—	ContinuousConstSMul Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane instTopologicalSpace SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction	—	continuous_induced_rng Continuous.comp continuous_id Complex.continuous_conj Continuous.div IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Continuous.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing Continuous.mul continuous_const continuous_coe denom_ne_zero
instContractibleSpace 📖	mathematical	—	ContractibleSpace UpperHalfPlane instTopologicalSpace	—	Homeomorph.contractibleSpace_iff isEmbedding_coe range_coe Convex.contractibleSpace IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_halfSpace_im_gt LT.lt.trans_eq one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike I_im
instLocPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace UpperHalfPlane instTopologicalSpace	—	Topology.IsOpenEmbedding.locPathConnectedSpace LocallyConvexSpace.toLocPathConnectedSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul NormedSpace.toLocallyConvexSpace isOpenEmbedding_coe
instLocallyCompactSpace 📖	mathematical	—	LocallyCompactSpace UpperHalfPlane instTopologicalSpace	—	Topology.IsOpenEmbedding.locallyCompactSpace locallyCompact_of_proper Complex.instProperSpace isOpenEmbedding_coe
instNoncompactSpace 📖	mathematical	—	NoncompactSpace UpperHalfPlane instTopologicalSpace	—	Topology.IsEmbedding.isCompact_iff isEmbedding_coe Set.image_univ range_coe Complex.closure_preimage_im closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instReflLe IsClosed.closure_eq IsCompact.isClosed Complex.instT2Space
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology UpperHalfPlane instTopologicalSpace	—	TopologicalSpace.secondCountableTopology_induced UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace
instT3Space 📖	mathematical	—	T3Space UpperHalfPlane instTopologicalSpace	—	Topology.IsEmbedding.t3Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space Complex.instT2Space CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity isEmbedding_coe
instT4Space 📖	mathematical	—	T4Space UpperHalfPlane instTopologicalSpace	—	instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space CompletelyNormalSpace.toNormalSpace CompletelyNormalSpace.of_regularSpace_secondCountableTopology T3Space.toRegularSpace instSecondCountableTopology
isEmbedding_coe 📖	mathematical	—	Topology.IsEmbedding UpperHalfPlane Complex instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField coe	—	Function.Injective.isEmbedding_induced coe_injective
isOpenEmbedding_coe 📖	mathematical	—	Topology.IsOpenEmbedding UpperHalfPlane Complex instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField coe	—	isEmbedding_coe range_coe
isOpenMap_im 📖	mathematical	—	IsOpenMap UpperHalfPlane Real instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace im	—	IsOpenMap.comp Complex.isOpenMap_im Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding_coe
isOpenMap_norm 📖	mathematical	—	IsOpenMap UpperHalfPlane Real instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm Complex Complex.instNorm coe	—	IsOpenMap.of_nhds_le Filter.mem_map_iff_exists_image Topology.IsOpenEmbedding.image_mem_nhds isOpenEmbedding_coe subset_trans Set.instIsTransSubset lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.norm_eq_abs mem_ball_iff_norm Mathlib.Tactic.Linarith.sub_nonpos_of_le mem_ball_iff_norm' sub_zero Complex.ofReal_sub Complex.ofReal_div Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one norm_mul NormedDivisionRing.toNormMulClass Complex.norm_real norm_norm sub_mul one_mul div_mul_cancel₀ ne_zero Set.mem_of_mem_of_subset norm_div Real.norm_of_nonneg
isOpenMap_re 📖	mathematical	—	IsOpenMap UpperHalfPlane Real instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace re	—	IsOpenMap.comp Complex.isOpenMap_re Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding_coe
mem_verticalStrip_iff 📖	mathematical	—	UpperHalfPlane Set Set.instMembership verticalStrip Real Real.instLE abs Real.lattice Real.instAddGroup re im	—	—
ofComplex_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Complex UpperHalfPlane UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex coe	—	Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv isOpenEmbedding_coe
ofComplex_apply_eq_ite 📖	mathematical	—	OpenPartialHomeomorph.toFun' Complex UpperHalfPlane UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex Real Real.instLT Real.instZero Complex.im Real.decidableLT instInhabited	—	ofComplex_apply LT.lt.not_ge im_pos
ofComplex_apply_eq_of_im_nonpos 📖	mathematical	Real Real.instLE Complex.im Real.instZero	OpenPartialHomeomorph.toFun' Complex UpperHalfPlane UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex	—	ofComplex_apply_of_im_nonpos
ofComplex_apply_of_im_nonpos 📖	mathematical	Real Real.instLE Complex.im Real.instZero	OpenPartialHomeomorph.toFun' Complex UpperHalfPlane UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex instInhabited	—	ofComplex_apply_eq_ite
ofComplex_apply_of_im_pos 📖	mathematical	Real Real.instLT Real.instZero Complex.im	OpenPartialHomeomorph.toFun' Complex UpperHalfPlane UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex	—	ofComplex_apply
subset_verticalStrip_of_isCompact 📖	mathematical	IsCompact UpperHalfPlane instTopologicalSpace	Real Real.instLT Real.instZero Set UpperHalfPlane Set.instHasSubset verticalStrip	—	Set.eq_empty_or_nonempty Real.zero_lt_one Set.empty_subset IsCompact.exists_isMaxOn instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.continuousOn Continuous.comp continuous_abs Real.instIsOrderedAddMonoid continuous_re IsCompact.exists_isMinOn instClosedIicTopology continuous_im im_pos isMaxOn_iff isMinOn_iff
verticalStrip_anti_right 📖	mathematical	Real Real.instLE	Set UpperHalfPlane Set.instHasSubset verticalStrip	—	verticalStrip_mono le_rfl
verticalStrip_mono 📖	mathematical	Real Real.instLE	Set UpperHalfPlane Set.instHasSubset verticalStrip	—	LE.le.trans
verticalStrip_mono_left 📖	mathematical	Real Real.instLE	Set UpperHalfPlane Set.instHasSubset verticalStrip	—	verticalStrip_mono le_rfl

---

← Back to Index