Skip to content

Add monotone-of-tendsto lemmas and OrderDual SupConvergenceClass instance #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
CoolRmal wants to merge 1 commit into from
Closed

Add monotone-of-tendsto lemmas and OrderDual SupConvergenceClass instance #7

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions Mathlib/Topology/Order/MonotoneConvergence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,29 @@ open scoped Topology

variable {α β : Type*}

section

variable [Preorder α] [TopologicalSpace β] [OrderClosedTopology β]
{ι : Type*} {l : Filter ι} {f : ι → α → β} {g : α → β}

/-- If a family of functions is eventually monotone and converges pointwise, then the limit
function is monotone. -/
theorem monotone_of_eventually_monotone_of_tendsto
(hmono : ∀ᶠ n in l, Monotone (f n))
(hlim : ∀ x, Tendsto (fun n ↦ f n x) l (𝓝 (g x))) :
Comment on lines +44 to +46

@chatgpt-codex-connector chatgpt-codex-connector Bot May 18, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Add NeBot assumption to monotone limit theorem

This theorem is currently stated for an arbitrary filter l, but it is false when l = ⊥: both hmono and each pointwise Tendsto hypothesis become vacuously true, so the lemma would force any g to be monotone. The result should require [NeBot l] (and the wrapper theorem should inherit it) so the assumptions are non-vacuous and match the intended use of le_of_tendsto-style order-closed arguments.

Useful? React with 👍 / 👎.

Monotone g := by
intro a b hab
exact le_of_tendsto (hlim a) (hlim b) <| hmono.mono fun _ hn ↦ hn hab

/-- If a family of monotone functions converges pointwise, then the limit function is monotone. -/
theorem monotone_of_tendsto
(hmono : ∀ n, Monotone (f n))
(hlim : ∀ x, Tendsto (fun n ↦ f n x) l (𝓝 (g x))) :
Monotone g :=
monotone_of_eventually_monotone_of_tendsto (Filter.Eventually.of_forall hmono) hlim

end

/-- We say that `α` is a `SupConvergenceClass` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a least upper bound of `Set.range f`. Then `f x` tends to `𝓝 a`
as `x → ∞` (formally, at the filter `Filter.atTop`). We require this for `ι = (s : Set α)`,
Expand Down
Loading