Theorems · Theorem · complex analysis
Complex.HadamardThreeLines.mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip
∀ {z : ℂ} {l u : ℝ},
l < u →
z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u →
z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1If z is on the closed strip re ⁻¹' [l, u], then (z - l) / (u - l) is on the closed strip
re ⁻¹' [0, 1].
- Defined in
- Mathlib.Analysis.Complex.Hadamard
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.cast_zeroproof · cited by 1,870
- Set.Iccproof · cited by 1,702
- Complex.ofRealstatement and proof · cited by 1,654
- le_of_ltproof · cited by 1,175
- sub_selfproof · cited by 996
Cited by2
Results whose statement or proof uses this declaration.
- Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip'proof · cited by 0