ProperAction

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

Statistics

Metric	Count
Definitions	0
Theorems continuous_toSL2R, instContinuousSMulGL2R, instContinuousSMulSL2R, instProperSMul, isProperMap_smul_I, σ_eventuallyEq	6
Total	6

UpperHalfPlane

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toSL2R 📖	mathematical	—	Continuous UpperHalfPlane Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing instTopologicalSpace Matrix.SpecialLinearGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toSL2R	—	continuous_induced_rng continuous_matrix Fintype.complete Continuous.comp Real.continuous_sqrt continuous_im Continuous.div₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_re Continuous.sqrt Real.sqrt_ne_zero' im_pos continuous_const coe_toSL2R one_div Matrix.cons_val' Matrix.cons_val_fin_one Continuous.inv₀
instContinuousSMulGL2R 📖	mathematical	—	ContinuousSMul Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction Units.instTopologicalSpaceUnits instTopologicalSpaceMatrix UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace	—	ContinuousAt.congr ContinuousAt.comp Continuous.continuousAt ContinuousAlgEquiv.continuous ContinuousAt.div₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing ContinuousAt.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousAt.mul Continuous.comp Complex.continuous_ofReal Continuous.matrix_elem continuous_id Units.continuous_val continuous_fst ContinuousAt.comp' continuous_coe ContinuousAt.snd continuousAt_id' denom_ne_zero Filter.mp_mem Filter.Eventually.prod_inl_nhds σ_eventuallyEq Filter.univ_mem' map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass
instContinuousSMulSL2R 📖	mathematical	—	ContinuousSMul Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring Matrix.SpecialLinearGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace	—	ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing ContinuousAt.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousAt.mul Continuous.continuousAt Continuous.comp Complex.continuous_ofReal Continuous.matrix_elem continuous_subtype_val continuous_fst ContinuousAt.comp' continuous_coe ContinuousAt.snd continuousAt_id' denom_ne_zero coe_specialLinearGroup_apply
instProperSMul 📖	mathematical	—	ProperSMul Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing UpperHalfPlane Matrix.SpecialLinearGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace Matrix.SpecialLinearGroup.instGroup SLAction Algebra.id CommRing.toCommSemiring	—	MulAction.properSMul_of_proper_orbitMap instContinuousSMulSL2R Matrix.SpecialLinearGroup.topologicalGroup instIsTopologicalRingReal isPretransitiveSL2R isProperMap_smul_I
isProperMap_smul_I 📖	mathematical	—	IsProperMap Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing UpperHalfPlane Matrix.SpecialLinearGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring I	—	isProperMap_iff_isCompact_preimage T25Space.t2Space T3Space.t25Space instT3Space to_compactlyCoherentSpace instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace instLocallyCompactSpace Continuous.smul instContinuousSMulSL2R continuous_id' continuous_const pi_properSpace instProperSpaceReal dist_zero_right ProperSpace.isCompact_closedBall Topology.IsClosedEmbedding.isCompact_preimage Matrix.SpecialLinearGroup.isClosedEmbedding_val instIsTopologicalRingReal T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal IsCompact.of_isClosed_subset IsClosed.preimage IsCompact.isClosed Fintype.complete le_trans Real.le_sqrt_of_sq_le sq_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add le_max_left le_max_right
σ_eventuallyEq 📖	mathematical	—	Filter.EventuallyEq Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring ContinuousAlgEquiv Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike nhds Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix Real.pseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring σ	—	IsOpen.mem_nhds IsOpen.preimage Continuous.matrix_det instIsTopologicalRingReal Units.continuous_val isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.mp_mem Filter.univ_mem' Real.instNontrivial isOpen_Iio instClosedIciTopology

---

← Back to Index