Stream: Is there code for X?

Topic: Extreme Value Theorem

James Spence (Dec 04 2023 at 18:17):

Has the Extreme Value Theorem been formalised in Isabelle/HOL?

Mohammad Abdulaziz (Dec 04 2023 at 18:36):

I think Limits.isCont_bounded should give you what you need. Did you look at it?

James Spence (Dec 04 2023 at 18:43):

I don't think that's strong enough for what I need, I need the bound to be as close as possible. But I may be able to use that to prove the extreme value theorem. Thank you

Mohammad Abdulaziz (Dec 04 2023 at 19:06):

See Limits.isCont_Lb_Ub

James Spence (Dec 04 2023 at 19:09):

Ooh yes that looks right, thank you!

Last updated: Dec 21 2024 at 16:20 UTC