Mathlib Map

Theorems · Theorem · general topology

UpperHalfPlane.continuous_coe

Continuous UpperHalfPlane.coe
Defined in
Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Cited by
4 results in Mathlib
Foundations
Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

UpperHalfPlane.continuous_im · cited by 4UpperHalfPlane.continuous…UpperHalfPlane.continuous_re · cited by 4UpperHalfPlane.continuous…ModularGroup.isClosed_fd · cited by 1ModularGroup.isClosed_fdModularGroup.isOpen_fdo · cited by 1ModularGroup.isOpen_fdoComplex · cited by 5565ComplexContinuous · cited by 2592ContinuousUpperHalfPlane · cited by 626UpperHalfPlaneUpperHalfPlane.coe · cited by 288UpperHalfPlane.coeTopology.IsEmbedding.continuous · cited by 51IsEmbedding.continuousUpperHalfPlane.isEmbedding_coe · cited by 5UpperHalfPlane.isEmbeddin…UpperHalfPlane.continuous_coeCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.