Theorems · Definition · complex analysis
Complex.UnitClosedDisc.mk
(z : ℂ) → ‖z‖ ≤ 1 → Complex.UnitClosedDisc
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
- 12 results in Mathlib
- Foundations
- Depth 139 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.UnitClosedDiscstatement · cited by 42
Cited by13
Results whose statement or proof uses this declaration.
- Complex.UnitClosedDisc.casesOnstatement and proof · cited by 1
- Complex.UnitClosedDisc.casesOn_mkstatement and proof · cited by 0
- Complex.UnitClosedDisc.coe_mkstatement · cited by 0
- Complex.UnitClosedDisc.mk.congr_simpstatement and proof · cited by 0
- Complex.UnitClosedDisc.mk_eq_onestatement · cited by 0
- Complex.UnitClosedDisc.existsstatement and proof · cited by 0
- Complex.UnitClosedDisc.forallstatement and proof · cited by 0
- Complex.UnitClosedDisc.mk_coestatement · cited by 0
- Complex.UnitClosedDisc.mk_eq_zerostatement · cited by 0
- Complex.UnitClosedDisc.mk_injstatement · cited by 0
- Complex.UnitClosedDisc.mk_negstatement · cited by 0
- Complex.UnitClosedDisc.mk_onestatement · cited by 0