Theorems · Theorem · complex analysis
Complex.HadamardThreeLines.diffContOnCl_interpStrip
∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
DiffContOnCl ℂ (Complex.HadamardThreeLines.interpStrip f) (Complex.HadamardThreeLines.verticalStrip 0 1)- Defined in
- Mathlib.Analysis.Complex.Hadamard
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- Complexstatement and proof · cited by 5,565
- DifferentiableAtproof · cited by 617
- lt_of_le_of_neproof · cited by 230
- DiffContOnClstatement and proof · cited by 92
- differentiableAt_idproof · cited by 63
- Complex.HadamardThreeLines.sSupNormImproof · cited by 19
- Differentiable.diffContOnClproof · cited by 15
- DifferentiableAt.const_subproof · cited by 14
- DifferentiableAt.mulproof · cited by 13
- Complex.HadamardThreeLines.verticalStripstatement and proof · cited by 13
Cited by1
Results whose statement or proof uses this declaration.