Topology

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

Statistics

Metric	Count
Definitions instTopologicalSpace, ofComplex, verticalStrip, «term↑ₕ_»	4
Theorems upperHalfPlaneMk, 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, 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	29
Total	33

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	UpperHalfPlane UpperHalfPlane.instTopologicalSpace	—	Topology.IsEmbedding.continuous_iff UpperHalfPlane.isEmbedding_coe

UpperHalfPlane

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	60 math math: mdifferentiable_num, CuspFormClass.holo, ModularFormClass.differentiableAt_comp_ofComplex, CuspFormClass.zero_at_infty_comp_ofComplex, isOpenEmbedding_coe, comp_ofComplex_of_im_pos, Continuous.upperHalfPlaneMk, comp_ofComplex, mdifferentiable_inv_denom, ofComplex_apply_of_im_nonpos, ModularFormClass.continuous, contMDiff_coe, CuspForm.holo', instLocPathConnectedSpace, contMDiff_inv_denom, instT4Space, instNoncompactSpace, ofComplex_apply_of_im_pos, instContractibleSpace, SlashInvariantFormClass.periodic_comp_ofComplex, contMDiff_num, mdifferentiable_denom, ofComplex_apply_eq_of_im_nonpos, ofComplex_apply_eq_ite, J_smul, contMDiff_denom_zpow, ofComplex_apply, instLocallyCompactSpace, IsZeroAtImInfty.zero_at_infty_comp_ofComplex, eventuallyEq_coe_comp_ofComplex, comp_ofComplex_of_im_le_zero, continuous_im, 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, contMDiff_smul, tendsto_comap_im_ofComplex, contMDiff_denom, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, mdifferentiable_denom_zpow, continuous_coe, mdifferentiable_iff, isEmbedding_coe, mdifferentiableAt_ofComplex, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, mdifferentiable_smul, ModularGroup.isCompact_truncatedFundamentalDomain, continuous_re
ofComplex 📖	CompOp	23 math math: ModularFormClass.differentiableAt_comp_ofComplex, CuspFormClass.zero_at_infty_comp_ofComplex, comp_ofComplex_of_im_pos, comp_ofComplex, ofComplex_apply_of_im_nonpos, ofComplex_apply_of_im_pos, 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, contMDiffAt_ofComplex, ModularFormClass.bounded_at_infty_comp_ofComplex, contMDiffAt_iff, EisensteinSeries.eisSummand_extension_differentiableOn, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, mdifferentiableAt_iff, tendsto_comap_im_ofComplex, 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
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
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 IsTopologicalSemiring.toContinuousAdd Continuous.mul continuous_const continuous_coe denom_ne_zero
instContractibleSpace 📖	mathematical	—	ContractibleSpace UpperHalfPlane instTopologicalSpace	—	Homeomorph.contractibleSpace_iff isEmbedding_coe range_coe Convex.contractibleSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring 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 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
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 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