Oppositely monotone functions with reversed endpoint order cross exactly once

Proved

BianchiIX.unique_crossing_of_opposite_monotonicity

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $s<t$ , and let $V,W:[s,t]\to\mathbb R$ be continuous, with $V$ strictly decreasing and $W$ strictly increasing. If $W(s)<V(s)$ and $V(t)<W(t)$ , then there is exactly one $r\in(s,t)$ with $V(r)=W(r)$ .

Preamble

import Mathlib.Topology.Order.IntermediateValue
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Tactic.Linarith

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set

Formal statement

theorem BianchiIX.unique_crossing_of_opposite_monotonicity {V W : ℝ → ℝ} {s t : ℝ}
    (hst : s < t) (hV : ContinuousOn V (Icc s t)) (hW : ContinuousOn W (Icc s t))
    (hVa : StrictAntiOn V (Icc s t)) (hWm : StrictMonoOn W (Icc s t))
    (hs : W s < V s) (ht : V t < W t) : ∃! r, r ∈ Ioo s t ∧ V r = W r := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/MonotoneCrossing.lean#L11-L41

View graph