The upper half plane #
This file defines UpperHalfPlane
to be the upper half plane in ℂ
.
We define the notation ℍ
for the upper half plane available in the locale
UpperHalfPlane
so as not to conflict with the quaternions.
The open upper half plane, denoted as ℍ
within the UpperHalfPlane
namespace
Instances For
The open upper half plane, denoted as ℍ
within the UpperHalfPlane
namespace
Equations
- UpperHalfPlane.termℍ = Lean.ParserDescr.node `UpperHalfPlane.termℍ 1024 (Lean.ParserDescr.symbol "ℍ")
Instances For
Equations
Equations
instance
UpperHalfPlane.canLift :
CanLift ℂ UpperHalfPlane UpperHalfPlane.coe fun (z : ℂ) => 0 < z.im
Imaginary part
Instances For
Extensionality lemma in terms of UpperHalfPlane.re
and UpperHalfPlane.im
.
Constructor for UpperHalfPlane
. It is useful if ⟨z, h⟩
makes Lean use a wrong
typeclass instance.
Equations
- UpperHalfPlane.mk z h = ⟨z, h⟩
Instances For
@[simp]
Define I := √-1 as an element on the upper half plane.
Instances For
Extension for the positivity
tactic: UpperHalfPlane.im
.
Instances For
Extension for the positivity
tactic: UpperHalfPlane.coe
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.