Theorems · Theorem · complex analysis
Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne
∀ (h : ℝ) (f : ℂ → ℂ),
Function.Periodic.cuspFunction h f 0 = (nhdsWithin 0 {0}ᶜ).limUnder (Function.Periodic.cuspFunction h f)- Defined in
- Mathlib.Analysis.Complex.Periodic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Compl.complstatement and proof · cited by 2,925
- nhdsWithinstatement and proof · cited by 1,912
- Function.update_selfproof · cited by 201
- Function.update_of_neproof · cited by 198
- Filter.limUnderstatement and proof · cited by 47
- Function.Periodic.invQParamproof · cited by 18
- Function.Periodic.cuspFunctionstatement and proof · cited by 18
- Filter.map_congrproof · cited by 10
- Filter.limproof · cited by 10
Cited by1
Results whose statement or proof uses this declaration.
- Function.Periodic.differentiableAt_cuspFunction_zeroproof · cited by 3