Theorems · Theorem · complex analysis

circleIntegral.integral_sub

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R →
    CircleIntegrable g c R → ∮ (z : ℂ) in C(c, R), f z - g z = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z

Defined in: Mathlib.MeasureTheory.Integral.CircleIntegral
Cited by: 4 results in Mathlib
Foundations: Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Complexstatement and proof · cited by 5,565
Real.piproof · cited by 1,774
MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
derivproof · cited by 676
intervalIntegralproof · cited by 546
smul_subproof · cited by 142
circleMapproof · cited by 117
CircleIntegrablestatement and proof · cited by 86
circleIntegralstatement · cited by 60

Cited by4

Results whose statement or proof uses this declaration.

Complex.cderiv_subproof · cited by 1
Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiableproof · cited by 1
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_auxproof · cited by 1
Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendstoproof · cited by 1