`Compfiles/UpperLowerContinuous.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

15 declarations, 0 contain sorry, 0 declared as axioms

Suppose f : ℝ -> ℝ is continuous in both the upper topology (where the basic open sets are half-open intervals (a, b]) and lower topology (where the basic open sets are half-open intervals [a,b)). Then f is continuous in the usual topology (where the basic open sets are open intervals (a,b)) and also monotone nondecreasing.

Imports (8)

Imported by 1 file

Compfiles.lean

def UpperLowerContinuous.upper_intervals line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, Exists, Eq, Set.Ioc
1 instances, coercions and auxiliary constants left out.
def UpperLowerContinuous.lower_intervals line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, Exists, Eq, Set.Ico
1 instances, coercions and auxiliary constants left out.
def UpperLowerContinuous.open_intervals line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, Exists, Eq, Set.Ioo
1 instances, coercions and auxiliary constants left out.
def UpperLowerContinuous.tᵤ Generate the toplogy on ℝ by intervals of the form (a, b] line 40 source
Source documentation
Generate the toplogy on ℝ by intervals of the form (a, b].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Real
Proof uses: TopologicalSpace.generateFrom, UpperLowerContinuous.upper_intervals
```
def tᵤ : TopologicalSpace ℝ := TopologicalSpace.generateFrom upper_intervals
…
```
Mentions: UpperLowerContinuous.upper_intervals
def UpperLowerContinuous.tₗ Generate the toplogy on ℝ by intervals of the form [a, b) line 44 source
Source documentation
Generate the toplogy on ℝ by intervals of the form [a, b).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Real
Proof uses: TopologicalSpace.generateFrom, UpperLowerContinuous.lower_intervals
```
def tₗ : TopologicalSpace ℝ := TopologicalSpace.generateFrom lower_intervals
…
```
Mentions: UpperLowerContinuous.lower_intervals
def UpperLowerContinuous.tₛ This should be equivalent to the default instance for TopologicalSpace ℝ, which goes through UniformSpace, but for now I don't want to bother with proving that equivalence line 51 source
Source documentation
This should be equivalent to the default instance for TopologicalSpace ℝ, which goes through UniformSpace, but for now I don't want to bother with proving that equivalence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Real
Proof uses: TopologicalSpace.generateFrom, UpperLowerContinuous.open_intervals
```
def tₛ : TopologicalSpace ℝ := TopologicalSpace.generateFrom open_intervals
…
```
Mentions: UpperLowerContinuous.open_intervals
lemma UpperLowerContinuous.real_induction Let S be a set of real numbers such that: 1 line 64 source
Source documentation
Let S be a set of real numbers such that:
1. If x ∈ S, then we can find y > x such that [x, y) ⊆ S.
2. If [x, y) ⊆ S, then y ∈ S. Then, given z ∈ S, we have [z, ∞) ⊆ S.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real, Membership.mem, Exists, And, LT.lt, LE.le, Set.Ico, Set.Ici
Proof uses: Classical.byContradiction, Not, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Set.subset_def, Set.ofPred, InfSet.sInf, Set.Nonempty, Exists.intro, And.intro, lowerBounds, And.left, BddBelow, Set.nonempty_of_mem, Iff.mpr, not_le and 15 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma real_induction
    {S : Set ℝ}
    (h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S)
    (h2 : ∀ x y, x < y → Set.Ico x y ⊆ S → y ∈ S)
    {z : ℝ}
    (hz : z ∈ S)
    : Set.Ici z ⊆ S := by
…
```
Mentions: S
lemma UpperLowerContinuous.lower_basis line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace.IsTopologicalBasis, Real, UpperLowerContinuous.tₗ, UpperLowerContinuous.lower_intervals
Proof uses: TopologicalSpace.IsTopologicalBasis.mk, Set, Membership.mem, Inter.inter, Exists, Eq, Set.Ico, And, LE.le, Exists.intro, Max.max, Min.min, And.intro, rfl, of_eq_true, Eq.trans, LT.lt, True, congr, congrArg and 13 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma UpperLowerContinuous.upper_basis line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace.IsTopologicalBasis, Real, UpperLowerContinuous.tᵤ, UpperLowerContinuous.upper_intervals
Proof uses: TopologicalSpace.IsTopologicalBasis.mk, Set, Membership.mem, Inter.inter, Exists, Eq, Set.Ioc, And, LE.le, Exists.intro, Max.max, Min.min, And.intro, rfl, of_eq_true, Eq.trans, LT.lt, True, congr, congrArg and 13 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma UpperLowerContinuous.open_basis line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace.IsTopologicalBasis, Real, UpperLowerContinuous.tₛ, UpperLowerContinuous.open_intervals
Proof uses: TopologicalSpace.IsTopologicalBasis.mk, Set, Membership.mem, Inter.inter, Exists, Eq, Set.Ioo, And, LE.le, Exists.intro, Max.max, Min.min, And.intro, rfl, of_eq_true, Eq.trans, LT.lt, True, congr, congrArg and 14 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma UpperLowerContinuous.continuous_of_upper_lower_continuous line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Continuous, UpperLowerContinuous.tᵤ, UpperLowerContinuous.tₗ, UpperLowerContinuous.tₛ
Proof uses: Iff.mpr, TopologicalSpace.generateFrom, UpperLowerContinuous.open_intervals, Set, Membership.mem, IsOpen, Set.preimage, continuous_generateFrom_iff, Exists, Eq, Set.Ioo, And, LE.le, Set.Ioc, LT.lt, TopologicalSpace.isOpen_generateFrom_of_mem, UpperLowerContinuous.upper_intervals, Exists.intro, rfl, Iff.mp and 25 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
lemma UpperLowerContinuous.infinite_interval_lower_open [x, ∞) is open in tₗ line 288 source
Source comment
[x, ∞) is open in tₗ

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, IsOpen, UpperLowerContinuous.tₗ, Set.Ici
Proof uses: Eq.mpr, Membership.mem, Set, Exists, And, UpperLowerContinuous.lower_intervals, LE.le, id, Eq, congrArg, propext, TopologicalSpace.IsTopologicalBasis.isOpen_iff, UpperLowerContinuous.lower_basis, Exists.intro, Set.Ico, HAdd.hAdd, OfNat.ofNat, And.intro, rfl, LT.lt and 6 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma infinite_interval_lower_open (x : ℝ) : IsOpen[tₗ] (Set.Ici x) := by
…
```
Mentions: UpperLowerContinuous.tₗ
lemma UpperLowerContinuous.infinite_interval_upper_open (-∞, x) is open in tᵤ line 306 source
Source comment
(-∞, x) is open in tᵤ

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, IsOpen, UpperLowerContinuous.tᵤ, Set.Iio
Proof uses: Eq.mpr, Membership.mem, Set, Exists, And, UpperLowerContinuous.upper_intervals, LE.le, id, Eq, congrArg, propext, TopologicalSpace.IsTopologicalBasis.isOpen_iff, UpperLowerContinuous.upper_basis, Exists.intro, Set.Ioc, HSub.hSub, OfNat.ofNat, And.intro, rfl, LT.lt and 6 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma infinite_interval_upper_open (x : ℝ) : IsOpen[tᵤ] (Set.Iio x) := by
…
```
Mentions: UpperLowerContinuous.tᵤ
theorem UpperLowerContinuous.monotone_of_upper_lower_continuous line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Continuous, UpperLowerContinuous.tᵤ, UpperLowerContinuous.tₗ, Monotone
Proof uses: LE.le, Membership.mem, Set, Set.preimage, Set.Ici, Exists, And, LT.lt, Set.Ico, IsOpen, Iff.mp, continuous_def, UpperLowerContinuous.infinite_interval_lower_open, UpperLowerContinuous.lower_intervals, TopologicalSpace.IsTopologicalBasis.isOpen_iff, UpperLowerContinuous.lower_basis, Eq, Exists.intro, And.intro, And.right and 117 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
problem UpperLowerContinuous.properties_of_upper_lower_continuous line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Continuous, UpperLowerContinuous.tᵤ, UpperLowerContinuous.tₗ, And, UpperLowerContinuous.tₛ, Monotone
Proof uses: And.intro, UpperLowerContinuous.continuous_of_upper_lower_continuous, UpperLowerContinuous.monotone_of_upper_lower_continuous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.