Zulip Chat Archive

Stream: Is there code for X?

Topic: Weierstrass Extreme Value Theorem

Pietro Monticone (Feb 22 2024 at 14:35):

Has the Weierstrass Extreme Value Theorem been formalized and included in Mathlib?

Ruben Van de Velde (Feb 22 2024 at 14:43):

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Order/Compact.html#IsCompact.exists_isMinOn

Last updated: May 02 2025 at 03:31 UTC