Skip to content
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.

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

feature(Order/ScottContinuity): Scott Continuity on product spaces #15412

Draft
wants to merge 257 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
257 commits
Select commit Hold shift + click to select a range
481671e
Remove redundant lemma
mans0954 May 26, 2024
340b971
Tidy up
mans0954 May 26, 2024
a98710f
Restore
mans0954 May 26, 2024
25d8b29
Fix
mans0954 May 26, 2024
33718ed
Better name
mans0954 May 26, 2024
e813aa1
Formatting
mans0954 May 26, 2024
46862d7
Fix
mans0954 May 26, 2024
423016a
Golf
mans0954 May 26, 2024
a2986a9
Fix
mans0954 May 26, 2024
ac965fe
Golf
mans0954 May 26, 2024
85f81a6
Golf
mans0954 May 26, 2024
3d237df
Golf
mans0954 May 26, 2024
54877af
Golf
mans0954 May 26, 2024
a24981f
Lint
mans0954 May 26, 2024
542efd9
Golf
mans0954 May 26, 2024
787d9a0
Golf
mans0954 May 26, 2024
bad53f4
Golf
mans0954 May 26, 2024
5fbd4f9
Golf
mans0954 May 26, 2024
277eddd
Merge branch 'master' into mans0954/Scott-unification
mans0954 May 27, 2024
295ec65
Update Mathlib/Order/Bounds/Basic.lean
mans0954 May 27, 2024
3204e1f
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
a5bde5c
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
4156352
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
4b6cde0
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
cd5afb7
Fix
mans0954 May 27, 2024
2129b80
Restore original def
mans0954 May 27, 2024
09492b3
Update Mathlib/Order/Bounds/Basic.lean
mans0954 May 27, 2024
bea537d
Update Mathlib/Order/Bounds/Basic.lean
mans0954 May 27, 2024
2bbec9d
Reorder terms
mans0954 May 27, 2024
164cfbe
Rename DScottContinuous to ScottContinuousOn
mans0954 May 27, 2024
870a54e
define the chain explicitly
mans0954 May 27, 2024
02224ad
ScottContinuous.scottContinuousOn
mans0954 May 27, 2024
31d7437
Add docstring
mans0954 May 27, 2024
85bf86b
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
ba593d2
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
cdf5c98
Fix
mans0954 May 27, 2024
80be6db
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 May 27, 2024
561f02d
WIP
mans0954 May 27, 2024
8ac8b54
Remove Continuous' definition
mans0954 May 27, 2024
137fb79
Rename lemmas
mans0954 May 28, 2024
84b3a7b
Fix
mans0954 May 28, 2024
e48077c
Fix
mans0954 May 28, 2024
5297af3
remove old aliases
mans0954 May 28, 2024
bb54fab
WiP
mans0954 May 28, 2024
99ac462
WiP
mans0954 May 28, 2024
179d2ad
Fudge around it for now
mans0954 May 28, 2024
6c34605
Golf
mans0954 May 28, 2024
e769b15
reset Order.OmegaCompletePartialOrder
YaelDillies May 29, 2024
cb928c1
split off Order.ScottContinuity, fix Order.OmegaCompletePartialOrder
YaelDillies May 29, 2024
cde4e47
feat: Monotonicity of monadic operations on `Part`
YaelDillies May 29, 2024
6b15c71
update Mathlib
YaelDillies May 29, 2024
6fd1323
sort imports
YaelDillies May 29, 2024
0cfbe0e
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jun 4, 2024
3607d43
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jun 7, 2024
b7e1311
chore(Order): More simp lemmas
YaelDillies May 29, 2024
8d4c935
Merge branch 'order_hom_mk_comp_mk' into mans0954/Scott-unification
mans0954 Jun 8, 2024
4fafac3
Topology
mans0954 Jun 9, 2024
8890cd4
Fix Order/Category/OmegaCompletePartialOrder
mans0954 Jun 9, 2024
ec395e0
Fix Topology/OmegaCompletePartialOrder
mans0954 Jun 9, 2024
f7c021c
Fix LawfulFix
mans0954 Jun 9, 2024
73c9c62
Fix
mans0954 Jun 9, 2024
2c6b5e5
Lint
mans0954 Jun 9, 2024
0c1dd9c
Clarify which Continuity in Topology/OmegaCompletePartialOrder
mans0954 Jun 9, 2024
0c70381
Some Continuous to ωScottContinuous
mans0954 Jun 9, 2024
901642a
Build without warnings
mans0954 Jun 9, 2024
211590b
Tidy up a bit
mans0954 Jun 9, 2024
0139a76
Tidy up some more
mans0954 Jun 9, 2024
0a12e13
Use named var
mans0954 Jun 13, 2024
a484e9f
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jun 13, 2024
8d51910
Merge branch 'master' into monotone_part_bind
mans0954 Jul 2, 2024
ff79021
Merge branch 'monotone_part_bind' into mans0954/Scott-unification
mans0954 Jul 3, 2024
fb49adb
Fix
mans0954 Jul 3, 2024
ed557ac
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 12, 2024
d39c56e
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 14, 2024
d90d737
Restore missing vars
mans0954 Jul 15, 2024
b1bf316
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 16, 2024
5e58f17
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 19, 2024
f8820b1
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 20, 2024
7206cfa
Remove align
mans0954 Jul 20, 2024
53440c8
Update Mathlib/Topology/Order/ScottTopology.lean
mans0954 Jul 20, 2024
ef20623
Update Mathlib/Topology/OmegaCompletePartialOrder.lean
mans0954 Jul 20, 2024
a48c85e
Update Mathlib/Control/LawfulFix.lean
mans0954 Jul 20, 2024
3a0dd59
Update Mathlib/Control/LawfulFix.lean
mans0954 Jul 20, 2024
1e1e899
Add missing alias
mans0954 Jul 20, 2024
44ed037
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 25, 2024
9d3df87
Fix
mans0954 Jul 25, 2024
a528979
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 Jul 27, 2024
d3f29b5
Lint
mans0954 Jul 27, 2024
f656c0d
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 Jul 27, 2024
82e6082
ite_Continuous' -> ite_ωScottContinuous
mans0954 Jul 27, 2024
059f960
Merge branch 'mans0954/Scott-unification' of github.com:leanprover-co…
mans0954 Jul 27, 2024
a0b2712
Update Mathlib/Topology/OmegaCompletePartialOrder.lean
mans0954 Jul 27, 2024
176df4f
Remove 'by exact'
mans0954 Jul 27, 2024
ab21676
Merge branch 'mans0954/Scott-unification' of github.com:leanprover-co…
mans0954 Jul 27, 2024
1b8a8be
Revert "ite_Continuous' -> ite_ωScottContinuous"
mans0954 Jul 27, 2024
07e9522
deprecate ite_continuous'
mans0954 Jul 27, 2024
771e97c
Order/ScottContinuity appears not to use γ or g
mans0954 Jul 28, 2024
03ad4da
Direct proof that mediating morphism of ωScottContinuous functions is…
mans0954 Jul 28, 2024
d3cb301
mediating morphism of ScottContinuous functions is ScottContinuous
mans0954 Jul 28, 2024
4728ba6
Update Mathlib/Order/OmegaCompletePartialOrder.lean
mans0954 Jul 28, 2024
4150887
Rename ScottContinuous.prodMk
mans0954 Jul 28, 2024
c8f22b6
Deduce ωScottContinuous.prodMk from the general case
mans0954 Jul 28, 2024
aefa938
Tidy
mans0954 Jul 28, 2024
41465ac
Show that the sup operation is Scott Continuous
mans0954 Jul 28, 2024
3856adf
Update Mathlib/Order/ScottContinuity.lean
mans0954 Jul 28, 2024
591c3b3
ScottContinuous.sup₂ -> ScottContinuousOn.sup₂
mans0954 Jul 28, 2024
754fb67
Merge branch 'master' into mans0954/Scott-unification
mans0954 Jul 30, 2024
e68f029
A function on a product space is monotone jointly if separately
mans0954 Jul 30, 2024
a0e17aa
Prod.upperBounds
mans0954 Jul 30, 2024
3c57858
Fix
mans0954 Jul 30, 2024
0b909da
IsLub
mans0954 Jul 31, 2024
011e533
Progress
mans0954 Jul 31, 2024
e699954
More fumbling
mans0954 Jul 31, 2024
ae41176
IsLUB.iUnion
mans0954 Aug 1, 2024
f5b09ca
upperBounds_iUnion
mans0954 Aug 1, 2024
6df37f8
Fix step1
mans0954 Aug 1, 2024
bec5191
step1'
mans0954 Aug 1, 2024
933d1f9
Progress
mans0954 Aug 1, 2024
d8e21aa
Merge branch 'master' into mans0954/scott-products
mans0954 Aug 1, 2024
ed7c273
Fix refine
mans0954 Aug 1, 2024
cca6d09
Finish lemma
mans0954 Aug 1, 2024
38ea7d6
Tidy
mans0954 Aug 1, 2024
f71f52d
Add a placeholder docstring
mans0954 Aug 1, 2024
90d8d6e
Refine
mans0954 Aug 1, 2024
4d4b1c1
ScottContinuous_prod_of_ScottContinuous
mans0954 Aug 1, 2024
32895ce
Tidy
mans0954 Aug 1, 2024
1adffae
ScottContinuity on complete lattices
mans0954 Aug 2, 2024
667b1b7
More fumbling
mans0954 Aug 2, 2024
6d10fa9
Right continuity of inf
mans0954 Aug 2, 2024
4f9788d
inf joint Scott continuity
mans0954 Aug 2, 2024
e413ff4
Lint
mans0954 Aug 2, 2024
70adfed
Simp
mans0954 Aug 2, 2024
b04d215
Refactor
mans0954 Aug 2, 2024
36cd44f
Directed products
mans0954 Aug 3, 2024
2616495
ScottContinuous no longer in Order/Directed
mans0954 Aug 3, 2024
9959fa1
Move DirectedOn product results
mans0954 Aug 3, 2024
2a4fb97
Pi projections
mans0954 Aug 4, 2024
c96374d
Merge branch 'master' into mans0954/scott-products
mans0954 Aug 4, 2024
7889d5f
Pi of directed
mans0954 Aug 7, 2024
73295ce
Namespace
mans0954 Aug 7, 2024
ea4122b
Fix
mans0954 Aug 8, 2024
4a408a2
Use existing monotone result
mans0954 Aug 8, 2024
13a3496
State Pi.upperBounds
mans0954 Aug 8, 2024
b4f67e8
Merge branch 'master' into mans0954/scott-products
mans0954 Aug 8, 2024
0ce73e6
Fix deprecated
mans0954 Aug 8, 2024
457dc8a
Replace Nat.or_exists_succ
mans0954 Aug 9, 2024
8eb5053
Golf Prod.upperBounds
mans0954 Aug 9, 2024
7b01d81
WiP
mans0954 Aug 9, 2024
bfc2903
Merge branch 'master' into mans0954/scott-products
mans0954 Aug 24, 2024
419d49c
Fix
mans0954 Aug 24, 2024
97886d6
Merge branch 'master' into mans0954/scott-products
mans0954 Aug 31, 2024
5cfd2ed
Merge branch 'master' into mans0954/scott-products
mans0954 Sep 5, 2024
31488db
Import CompleteLattice
mans0954 Sep 5, 2024
486c4e7
Fixes
mans0954 Sep 5, 2024
cad8d5f
Fix
mans0954 Sep 5, 2024
93b62b3
Fix merge
mans0954 Sep 5, 2024
5eeb324
Merge branch 'master' into mans0954/scott-products
mans0954 Sep 7, 2024
3c8b4c9
Merge branch 'master' into mans0954/scott-products
mans0954 Sep 13, 2024
da35949
Merge branch 'master' into mans0954/scott-products
mans0954 Sep 20, 2024
9a2813d
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 11, 2024
9a9e03d
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 12, 2024
7fdaad2
Remove files committed in error
mans0954 Oct 12, 2024
979d399
Lint
mans0954 Oct 13, 2024
e67ef9c
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 14, 2024
6cd8da6
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 15, 2024
c549fbc
Fix
mans0954 Oct 15, 2024
82a44b5
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 20, 2024
65b7358
Fix
mans0954 Oct 20, 2024
80dcc59
Merge branch 'master' into mans0954/scott-products
mans0954 Oct 27, 2024
d0f2543
Fix
mans0954 Oct 27, 2024
e48ca09
Merge branch 'master' into mans0954/scott-products
mans0954 Nov 1, 2024
5f53bd1
Merge branch 'master' into mans0954/scott-products
mans0954 Nov 7, 2024
5e2c4ea
Note to self
mans0954 Nov 17, 2024
23dd7f4
Golf
mans0954 Nov 17, 2024
98a3c63
Merge branch 'master' into mans0954/scott-products
mans0954 Nov 17, 2024
ae798c0
Golf
mans0954 Nov 17, 2024
15719d4
Mpre golf
mans0954 Nov 17, 2024
37fd45c
One more golf
mans0954 Nov 17, 2024
affadb8
Import Lattice from scott-products
mans0954 Nov 17, 2024
a27915f
Add Order/Bounds/Lattice to Mathlib.lean
mans0954 Nov 17, 2024
9e1125a
Add IsGLB.iUnion
mans0954 Nov 17, 2024
aa61cc9
update docstring
mans0954 Nov 17, 2024
8bd9665
Relabel α
mans0954 Nov 17, 2024
4a1650e
Don't need t
mans0954 Nov 18, 2024
d33d8de
Merge branch 'master' into mans0954/bounds_iUnion
mans0954 Nov 22, 2024
74add92
Merge branch 'master' into mans0954/scott-products
mans0954 Nov 22, 2024
e71cf30
Merge branch 'master' into mans0954/bounds_iUnion
mans0954 Nov 29, 2024
a5cf0b1
Merge branch 'master' into mans0954/scott-products
mans0954 Nov 29, 2024
767568a
Merge branch 'master' into mans0954/bounds_iUnion
mans0954 Dec 8, 2024
4031fb8
Merge branch 'master' into mans0954/scott-products
mans0954 Dec 8, 2024
e325237
Merge branch 'master' into mans0954/bounds_iUnion
mans0954 Dec 19, 2024
49639ae
Merge branch 'master' into mans0954/scott-products
mans0954 Dec 19, 2024
f9c3758
Merge branch 'master' into mans0954/scott-products
mans0954 Dec 21, 2024
89dca47
Fix
mans0954 Dec 21, 2024
6afe651
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
ce7d17a
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
47e84f5
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
fa4a21b
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
56af63f
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
b274f89
Update Mathlib/Order/Bounds/Lattice.lean
mans0954 Dec 24, 2024
7acb842
isGLB_iUnion_iff_of_isLUB
mans0954 Dec 24, 2024
d39f5e0
Move is*_congr
mans0954 Dec 24, 2024
c84f43f
Other half of move
mans0954 Dec 24, 2024
3887c7d
Update implementation notes
mans0954 Dec 24, 2024
e9abe91
Merge branch 'master' into mans0954/bounds_iUnion
mans0954 Dec 24, 2024
6e7931f
Merge branch 'mans0954/bounds_iUnion' into mans0954/scott-products
mans0954 Dec 25, 2024
cdeb40e
Fix
mans0954 Dec 26, 2024
32e1b16
Merge branch 'master' into mans0954/scott-products
mans0954 Dec 26, 2024
b6524dd
Monotone.jointly_of_separately
mans0954 Dec 26, 2024
48df9ee
Monotone.separately_iff_jointly
mans0954 Dec 26, 2024
cb6fffa
Antitone.separately_iff_jointly
mans0954 Dec 26, 2024
0575af1
Possible improvement?
mans0954 Dec 26, 2024
3bb401d
Merge branch 'mans0954/monotone-jointly_of_separately' into mans0954/…
mans0954 Dec 26, 2024
9aef480
Whitespace
mans0954 Dec 26, 2024
340a623
Get name right
mans0954 Dec 26, 2024
0d0051c
Merge branch 'mans0954/monotone-jointly_of_separately' into mans0954/…
mans0954 Dec 26, 2024
80e4938
Fix
mans0954 Dec 26, 2024
81624d5
Golf
mans0954 Dec 26, 2024
5dd9b01
Move things around
mans0954 Dec 26, 2024
1ebbcfe
New helper lemma
mans0954 Dec 26, 2024
a5ee7c1
Meddle
mans0954 Dec 26, 2024
7492ebd
Fix
mans0954 Dec 26, 2024
0d92350
Merge branch 'master' into mans0954/scott-products
mans0954 Jan 3, 2025
0be561e
Merge branch 'master' into mans0954/scott-products
mans0954 Jan 9, 2025
11b63f9
Merge branch 'master' into mans0954/scott-products
mans0954 Jan 18, 2025
d5bfb84
Merge branch 'master' into mans0954/scott-products
mans0954 Jan 22, 2025
1f08afb
Merge branch 'master' into mans0954/scott-products
mans0954 Feb 3, 2025
143b968
Fix
mans0954 Feb 3, 2025
9a32acd
Golf
mans0954 Feb 5, 2025
1ae9e5f
Golf
mans0954 Feb 5, 2025
2853c81
Any clearer?
mans0954 Feb 5, 2025
f6d1e7e
Revert "Any clearer?"
mans0954 Feb 5, 2025
7185eec
Golf
mans0954 Feb 5, 2025
5304c43
Golf some more
mans0954 Feb 5, 2025
1f93c4c
Decompose into lemmas
mans0954 Feb 5, 2025
659a7e4
Golf a bit more
mans0954 Feb 5, 2025
594a7c5
Golf some more
mans0954 Feb 5, 2025
25b5006
Break it down further
mans0954 Feb 5, 2025
4092bd3
Golf some more
mans0954 Feb 6, 2025
1740e88
Remove unnecessary lemma
mans0954 Feb 6, 2025
c505692
DirectedOn.prod_all_dominated
mans0954 Feb 6, 2025
9cbb274
upperBounds_eq_ofSubset
mans0954 Feb 6, 2025
37621dc
upperBounds_image_eq_ofSubset
mans0954 Feb 6, 2025
f3e4e3d
subset_fst_image_times_snd_image
mans0954 Feb 6, 2025
e840843
Monotone.upperBounds_image_of_directedOn_prod
mans0954 Feb 6, 2025
c1acd56
Merge branch 'mans0954/directed-prod-LUB' into mans0954/scott-products
mans0954 Feb 6, 2025
8858d74
Remove dup
mans0954 Feb 6, 2025
6fe02a6
Remove dup
mans0954 Feb 6, 2025
b8b169f
Fix
mans0954 Feb 6, 2025
c9fef62
Merge branch 'master' into mans0954/scott-products
mans0954 Feb 9, 2025
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
Prev Previous commit
Next Next commit
Fix refine
mans0954 committed Aug 1, 2024
commit ed7c27361025f97afec96f1c14b970da802f53eb
4 changes: 2 additions & 2 deletions Mathlib/Order/ScottContinuity.lean
Original file line number Diff line number Diff line change
@@ -37,8 +37,8 @@ lemma ScottContinuousOn.mono (hD : D₁ ⊆ D₂) (hf : ScottContinuousOn D₂ f

protected theorem ScottContinuousOn.monotone (D : Set (Set α)) (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D)
(h : ScottContinuousOn D f) : Monotone f := by
refine' fun a b hab =>
(h (hD a b hab) (insert_nonempty _ _) (directedOn_pair le_refl hab) _).1
refine fun a b hab =>
(h (hD a b hab) (insert_nonempty _ _) (directedOn_pair le_refl hab) ?_).1
(mem_image_of_mem _ <| mem_insert _ _)
rw [IsLUB, upperBounds_insert, upperBounds_singleton,
inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]