Theorem isPreconnected_uIoc

Modification history

2026-01-05 16:12

Mathlib/Topology/Order/IntermediateValue.lean

feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals (#30344) …

Added isPreconnected_uIoc View on Github →