mean value theorem for integration

Stream: Is there code for X?

[Adhyayan Sharma]

Is there any existing theorem in mathlib for MVT for integrals please? I went through the undergraduate maths section for Lean but couldn't find it

[Aaron Liu]

What is the statement you want?

[Adhyayan Sharma]

i wish to prove explicitly that $\int_a^b f(x)\,dx = f(c)\,(b - a)$, for a continuous function f and c in the closed interval [a,b], but was wondering if this is an existing theorem in mathlib thank you

[Aaron Liu]

I don't see it

[Adhyayan Sharma]

no worries! I'll try and formalise this proof by myself, thank you for looking!

[Aaron Liu]

It shouldn't be too hard