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.

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

Jump to bottom

Golf proofs and fix typos #21

Merged
merged 37 commits into from
May 16, 2024
Merged

Golf proofs and fix typos #21

merged 37 commits into from
May 16, 2024

Conversation

pitmonticone
Copy link
Collaborator

@pitmonticone pitmonticone commented May 8, 2024 •
edited
Loading

  • Golf proof of periodicpts_is_mem
  • Golf proof of periodic_arbitrary_large_time
  • Golf proof of inter_subset_empty_of_inter_empty
  • Golf proof of separated_balls
  • Golf proof of separated_ball_image_ball
  • Golf proof of separated_balls_along_non_periodic_orbit
  • Golf proof of ball_non_periodic_arbitrary_large_time
  • Golf proof of non_periodic_arbitrary_large_time
  • Golf proof of arbitrary_large_time
  • Golf proof of is_closed
  • Golf proof of is_cpt
  • Golf proof of omegaLimit_nonempty
  • Golf proof of omegaLimit_nonwandering
  • Golf proof of nonWandering_nonempty
  • Golf proof of recurrentSet_iff_accumulation_point
  • Golf proof of periodicpts_mem_recurrentSet
  • Golf proof of recurrentSet_nonwandering
  • Golf proof of recurrentSet_of_minimal_is_all_space
  • Golf proof of minimalSubset_mem_recurrentSet

pitmonticone and others added 2 commits May 8, 2024 21:52
@pitmonticone @LorenzoLuccioli
Fix typos in comments
abb2dc9 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Simplify proofs
6be06bf 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
mseri
mseri reviewed May 8, 2024
View reviewed changes
BET/Topological.lean
have hfnC : Continuous f^[n] := Continuous.iterate hf n
have hfx2' : x ≠ f^[n] x := Ne.symm hfx2
exact separated_balls (f^[n]) hfnC x hfx2'
lemma separated_ball_image_ball (n : ℕ) (hn : 0 < n) (x : α) (hfx : IsNotPeriodicPt f x) :
Copy link
Owner

Choose a reason for hiding this comment

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

Is there a particular reason to avoid using have or intros?

Copy link
Collaborator Author

@pitmonticone pitmonticone May 8, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Not really. It's just that in this case we could shorten the proof by removing them.

pitmonticone and others added 5 commits May 8, 2024 22:44
@pitmonticone @LorenzoLuccioli
Golf proof of separated_balls_along_non_periodic_orbit
2f83ff2 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf proof of ball_non_periodic_arbitrary_large_time
dd9282f 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone
Merge pull request #1 from mseri/main
af83bfa 
Update toolchain and manifest
@pitmonticone
Update Topological.lean
0f46267
@pitmonticone
Update Topological.lean
c47592e
@pitmonticone pitmonticone marked this pull request as draft May 9, 2024 20:04
pitmonticone and others added 21 commits May 9, 2024 22:18
@pitmonticone @LorenzoLuccioli
Golf non_periodic_arbitrary_large_time
7c5669e 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf arbitrary_large_time
616c0aa 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf is_closed
8f3fbb2 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
5ed3020 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
1a72ba9 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf is_cpt
6e289eb 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf omegaLimit_nonempty
e521529 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
a63d772 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf nonWandering_nonempty
40d9900 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
f683efb 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf recurrentSet_iff_accumulation_point
233428c 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
34fbb01 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
9b86a28 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
185ef88 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
c0072af 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
64a0e33 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
7df5c0d 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Remove dones
b7740de 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf recurrentSet_nonwandering
0539513 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Update Topological.lean
1e3e041 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf recurrentSet_of_minimal_is_all_space
c7b21f1 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
pitmonticone and others added 3 commits May 10, 2024 01:10
@pitmonticone @LorenzoLuccioli
Golf example
aecf166 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf example
5a0974c 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone @LorenzoLuccioli
Golf minimalSubset_mem_recurrentSet
274aaca 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
@pitmonticone pitmonticone marked this pull request as ready for review May 9, 2024 23:37
@pitmonticone @LorenzoLuccioli
Fix "unused variable minimality"
b3eba83 
Co-Authored-By: Lorenzo Luccioli <71074618+lorenzoluccioli@users.noreply.github.com>
mseri
mseri reviewed May 14, 2024
View reviewed changes
BET/Topological.lean Outdated Show resolved Hide resolved
mseri
mseri reviewed May 14, 2024
View reviewed changes
BET/Topological.lean Outdated Show resolved Hide resolved
mseri
mseri reviewed May 14, 2024
View reviewed changes
BET/Topological.lean Outdated Show resolved Hide resolved
mseri
mseri reviewed May 14, 2024
View reviewed changes
BET/Topological.lean Outdated Show resolved Hide resolved
mseri
mseri reviewed May 14, 2024
View reviewed changes
BET/Topological.lean Outdated Show resolved Hide resolved
pitmonticone and others added 5 commits May 14, 2024 22:21
@pitmonticone @mseri
Update BET/Topological.lean
944e8af 
Co-authored-by: Marcello Seri <mseri@users.noreply.github.com>
@pitmonticone @mseri
Update BET/Topological.lean
f5cdb57 
Co-authored-by: Marcello Seri <mseri@users.noreply.github.com>
@pitmonticone @mseri
Update BET/Topological.lean
c04ccc0 
Co-authored-by: Marcello Seri <mseri@users.noreply.github.com>
@pitmonticone @mseri
Update BET/Topological.lean
eded4dd 
Co-authored-by: Marcello Seri <mseri@users.noreply.github.com>
@pitmonticone @mseri
Update BET/Topological.lean
82bee8a 
Co-authored-by: Marcello Seri <mseri@users.noreply.github.com>
@mseri
Copy link
Owner

mseri commented May 16, 2024

Thanks for the PR! We looked at it with @oliver-butterley and we think it is time to merge :)

@mseri mseri merged commit f06dc4e into mseri:main May 16, 2024
1 check passed
@oliver-butterley
Copy link
Collaborator

Thanks @pitmonticone and @LorenzoLuccioli!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mseri mseri mseri left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@pitmonticone @mseri @oliver-butterley