Theorems · Definition · field theory
Complex.Rectangle
ℂ → ℂ → Set ℂ
A Rectangle is an axis-parallel rectangle with corners z and w.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Complexstatement and proof · cited by 5,565
- Complex.reproof · cited by 882
- Complex.improof · cited by 591
- Set.uIccproof · cited by 393
- Complex.reProdImproof · cited by 39
Cited by6
Results whose statement or proof uses this declaration.
- Complex.IsConservativeOnproof · cited by 7
- Complex.IsConservativeOn.monoproof · cited by 2
- DifferentiableOn.isConservativeOnproof · cited by 2
- Complex.rectangle_eq_convexHullstatement · cited by 1
- Complex.Convex.rectangle_subsetstatement · cited by 1
- Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegralproof · cited by 1