Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Increasing on a uniform above-above window

Proved
Monotonicity_Theorem.increasing_of_uniform_above_above2

by Tamas Fulop · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologyo-minimality

If every point of a window has an above-above sign pattern, some subwindow has the function strictly increasing. The difficult above case of Lemma 2. Retired: the window was not required to be nonempty, so the statement is false as stated; use Monotonicity_Theorem.increasing_of_uniform_above_above_corrected instead. Further retired 2026-09-14: old-framework statement superseded by the same-named new-framework formalization in the current staging proposal; the _corrected successor names are retired, use the clean names.

Preamble
import Definitions.Def_Monotonicity_Theorem_Framework2
Formal statement
theorem Monotonicity_Theorem.increasing_of_uniform_above_above2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R]
    (M : OMinimalStructure R) {I B : Set (Power R 1)}
    (f : DefinableFunction M I B)
    (hinj : ∀ x y (hx : I x) (hy : I y),
      f.toFun (Subtype.mk x hx) = f.toFun (Subtype.mk y hy) → x = y)
    {a b : Endpoint R} (hsubJ : ∀ x, openInterval a b x → I x)
    (hlt : Endpoint.lt a b)
    (hU : ∀ x (hxI : I x), openInterval a b x ->
        ∃ c1 c2 : Power R 1, openInterval a b c1 ∧ openInterval a b c2 ∧
        Lt1 c1 x ∧ Lt1 x c2 ∧
        (∀ y (hyI : I y), openInterval a b y → Lt1 c1 y → Lt1 y x ->
          Lt1 (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1) ∧
        (∀ y (hyI : I y), openInterval a b y → Lt1 x y → Lt1 y c2 ->
          Lt1 (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1)) :
    ∃ a2 b2 : Endpoint R, Endpoint.lt a2 b2 ∧
      (∀ x, openInterval a2 b2 x → I x) ∧
      (∀ x (hxI : I x) y (hyI : I y), openInterval a2 b2 x → openInterval a2 b2 y ->
        Lt1 x y → Lt1 (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1) := by sorry
Source
van den Dries, Tame Topology and O-Minimal Structures, Ch. 3
Read-back

What the Lean code literally says, in plain math · muse-spark

Fix a type RRR equipped with a linear order that is dense and has no maximum and no minimum, let MMM be an o-minimal structure on RRR, let III and BBB be sets of unary tuples over RRR, let fff be an MMM-definable function from III to BBB, and let aaa and bbb be endpoints over RRR; assume fff is injective in the sense that for any unary tuples x,yx,yx,y belonging to III, equality of the fff-values at xxx and yyy implies x=yx=yx=y, assume every unary tuple lying in the open interval (a,b)(a,b)(a,b) belongs to III, assume the left endpoint aaa is strictly below the right endpoint bbb, and assume the following uniform two-sided local lower-bound property: for every xxx belonging to III and also to (a,b)(a,b)(a,b) there exist unary tuples c1,c2c_1,c_2c1​,c2​ both in (a,b)(a,b)(a,b) with c1<x<c2c_1<x<c_2c1​<x<c2​ in the strict order on unary tuples such that, first, for every yyy belonging to III and to (a,b)(a,b)(a,b) with c1<y<xc_1<y<xc1​<y<x the scalar component of the fff-value at xxx is strictly less than the scalar component of the fff-value at yyy, and second, for every yyy belonging to III and to (a,b)(a,b)(a,b) with x<y<c2x<y<c_2x<y<c2​ the scalar component of the fff-value at xxx is strictly less than the scalar component of the fff-value at yyy; then there exist endpoints a2a_2a2​ and b2b_2b2​ with a2a_2a2​ strictly below b2b_2b2​ such that every unary tuple in the open interval (a2,b2)(a_2,b_2)(a2​,b2​) belongs to III and fff is strictly increasing on I∩(a2,b2)I\cap (a_2,b_2)I∩(a2​,b2​) in the sense that for any x,yx,yx,y belonging to III and to (a2,b2)(a_2,b_2)(a2​,b2​) with xxx strictly below yyy, the scalar component of the fff-value at xxx is strictly below that at yyy, where the universal claims are vacuously true if the relevant intersections I∩(a,b)I\cap(a,b)I∩(a,b) or I∩(a2,b2)I\cap(a_2,b_2)I∩(a2​,b2​) contain zero or one point, while the hypotheses that (a,b)(a,b)(a,b) is nondegenerate and contained in III normally force I∩(a,b)I\cap(a,b)I∩(a,b) to be nonempty in a dense order without ends.

Human review
  • Endorsed by Shuze Chen · Sep 15, 2026

  • Endorsed by Tamas Fulop · Sep 15, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me