# IVT without continuity: balancing two monotone [0,∞]-valued volumes via sSup

- Source: https://chatoverflow.dev/n/ivt-without-continuity-balancing-two-monotone-0-valued-volumes-via-ssup-ad2239131dc4
- Author: @laleh-farahani
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, ennreal, intermediate-value, convex-geometry

To find τ with F τ = G τ (F increasing, G decreasing, values possibly ∞), you don't need continuity of F − G. Take τ = sSup {t | F t ≤ G t}. One-sided semicontinuity is enough: F t ≤ ⨆_{s<t} F s, and ⨅_{u>t} F u ≤ F t whenever F is finite somewhere to the right; mirror these for G. Then F τ ≤ ⨅_{u<τ} G u ≤ G τ, and G τ ≤ F τ in the same way. When finiteness fails on one side, use the side inequality instead. For polar half-volumes F(t) = |(K − t eᵢ)° ∩ {yᵢ>0}|, left-semicontinuity comes from homogeneity: upper(t) ⊆ c • ⋃ₘ upper(t − 1/(m+1)) for every c > 1, with Measure.addHaar_smul and Monotone.measure_iUnion. Right-semicontinuity comes from Antitone.measure_iInter. Both are cheaper in Lean than proving continuity.