Skip to content

[Merged by Bors] - feat: generalize some results for SupConvergenceClass to ConditionallyCompletePartialOrder{Sup,Inf} #35050

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
j-loreaux wants to merge 13 commits into from
+7 −4
Closed

[Merged by Bors] - feat: generalize some results for SupConvergenceClass to ConditionallyCompletePartialOrder{Sup,Inf} #35050

Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7acc24b
feat: define `ConditionallyCompletePartialOrder`
j-loreaux Feb 9, 2026
b050f72
feat: basic API for `ConditionallyCompletePartialOrder`
j-loreaux Feb 9, 2026
87e6463
feat: generalize some `SupConvergenceClass` results to `Conditionally…
j-loreaux Feb 9, 2026
2390ddd
compare to `CompletePartialOrder`
j-loreaux Feb 9, 2026
2decfbd
fix missing `simp`
j-loreaux Feb 9, 2026
928c8b9
update module documentation
j-loreaux Feb 11, 2026
63827c9
Merge branch 'master' into CCPO-def
j-loreaux Feb 13, 2026
595462b
Merge branch 'CCPO-def' into CCPO-basic
j-loreaux Feb 13, 2026
eda5b56
add results on indexed suprema
j-loreaux Feb 16, 2026
4a6daef
move `WithBot` and `WithTop`
j-loreaux Feb 16, 2026
086cbab
imports
j-loreaux Feb 16, 2026
92045a0
Merge branch 'master' into CCPO-basic
j-loreaux Feb 16, 2026
49fd2b7
Merge branch 'CCPO-basic' into CCPO-convergence
j-loreaux Feb 16, 2026
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
11 changes: 7 additions & 4 deletions Mathlib/Topology/Order/MonotoneConvergence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,12 +111,15 @@ end IsGLB

section CiSup

variable [ConditionallyCompleteLattice α] [SupConvergenceClass α] {f : ι → α}
variable [ConditionallyCompletePartialOrderSup α] [SupConvergenceClass α] {f : ι → α}

theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
Tendsto f atTop (𝓝 (⨆ i, f i)) := by
cases isEmpty_or_nonempty ι
exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)]
obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)
· simp [h]
· obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
exact tendsto_atTop_isLUB h_mono <|
h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1
Expand All @@ -125,7 +128,7 @@ end CiSup

section CiInf

variable [ConditionallyCompleteLattice α] [InfConvergenceClass α] {f : ι → α}
variable [ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {f : ι → α}

theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
Tendsto f atBot (𝓝 (⨅ i, f i)) := by convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1
Expand Down
Loading
⚡