Theorems · Definition · complex analysis
Complex.UnitDisc.mk
(z : ℂ) → ‖z‖ < 1 → Complex.UnitDisc
A constructor that assumes ‖z‖ < 1 instead of dist z 0 < 1 and returns an element
of 𝔻 instead of ↥Metric.ball (0 : ℂ) 1.
- Defined in
- Mathlib.Analysis.Complex.UnitDisc.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- Complex.UnitDiscstatement · cited by 52
Cited by11
Results whose statement or proof uses this declaration.
- Complex.UnitDisc.casesOnstatement and proof · cited by 1
- Complex.UnitDisc.mk_coestatement · cited by 0
- Complex.UnitDisc.mk_eq_zerostatement · cited by 0
- Complex.UnitDisc.mk_injstatement · cited by 0
- Complex.UnitDisc.mk_negstatement · cited by 0
- Complex.UnitDisc.existsstatement and proof · cited by 0
- Complex.UnitDisc.mk_zerostatement · cited by 0
- Complex.UnitDisc.forallstatement and proof · cited by 0
- Complex.UnitDisc.casesOn_mkstatement and proof · cited by 0
- Complex.UnitDisc.mk.congr_simpstatement and proof · cited by 0
- Complex.UnitDisc.coe_mkstatement · cited by 0