HalfPlane

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

Statistics

Metric	Count
Definitions	0
Theorems isOpen_im_gt_EReal, isOpen_im_lt_EReal, isOpen_re_gt_EReal, isOpen_re_lt_EReal	4
Total	4

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_im_gt_EReal 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal im	—	isOpen_lt OrderTopology.to_orderClosedTopology EReal.instOrderTopology continuous_const EReal.continuous_coe_iff continuous_im
isOpen_im_lt_EReal 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal im	—	isOpen_lt OrderTopology.to_orderClosedTopology EReal.instOrderTopology EReal.continuous_coe_iff continuous_im continuous_const
isOpen_re_gt_EReal 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal re	—	isOpen_lt OrderTopology.to_orderClosedTopology EReal.instOrderTopology continuous_const EReal.continuous_coe_iff continuous_re
isOpen_re_lt_EReal 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal re	—	isOpen_lt OrderTopology.to_orderClosedTopology EReal.instOrderTopology EReal.continuous_coe_iff continuous_re continuous_const

---

← Back to Index