[Merged by Bors] - feat(topology/algebra/floor_ring): add basic topological facts about floor, ceil and fract
#4042
Conversation
ADedecker
added
the
awaiting-review
src/algebra/floor.lean
Outdated
| @@ -115,6 +116,9 @@ begin | |||
| exact ⟨floor_le v, lt_floor_add_one v⟩ | |||
| end | |||
|
|
|||
| lemma floor_eq_on_Ico (n : ℤ) : ∀ x ∈ (set.Ico n (n+1) : set α), (n : α) = floor x := | |||
There was a problem hiding this comment.
Is there a reason to put the complicated version on the right-hand side? Did you need to rewrite in this direction?
There was a problem hiding this comment.
It's a bit easier to use with e.g tendsto_nhds_within_congr, which assumes you now the limit of the left side. But that's not that important, I prefer reversing it.
src/algebra/floor.lean
Outdated
| by rw [←ceil_le, ←int.cast_one, ←int.cast_sub, ←lt_ceil, | ||
| int.sub_one_lt_iff, le_antisymm_iff, and.comm] | ||
|
|
||
| lemma ceil_eq_on_Ioc (n : ℤ) : ∀ x ∈ (set.Ioc (n-1) n : set α), (n:α) = ceil x := |
src/topology/algebra/floor_ring.lean
Outdated
| filter.tendsto (floor : α → ℤ) filter.at_top filter.at_top := | ||
| begin | ||
| refine monotone.tendsto_at_top_at_top (λ a b hab, floor_mono hab) (λ b, _), | ||
| use (b:α)+((1:ℤ):α), |
There was a problem hiding this comment.
| use (b:α)+((1:ℤ):α), | |
| use (b : α) + ((1 : ℤ) : α), |
src/topology/algebra/floor_ring.lean
Outdated
| variables {α : Type*} [linear_ordered_ring α] [floor_ring α] | ||
|
|
||
| lemma tendsto_floor_at_top : | ||
| filter.tendsto (floor : α → ℤ) filter.at_top filter.at_top := |
There was a problem hiding this comment.
Why not opening the filter namespace and remove all those filter.?
| filter.tendsto (floor : α → ℤ) filter.at_bot filter.at_bot := | ||
| begin | ||
| refine monotone.tendsto_at_bot_at_bot (λ a b hab, floor_mono hab) (λ b, ⟨b, _⟩), | ||
| rw floor_coe |
There was a problem hiding this comment.
Should exact_mod_cast help you here? floor_coe sounds like the name of a norm_cast lemma.
There was a problem hiding this comment.
It doesn't but that's not surprising : floor_coe isn't really a coe-manipulation lemma, it just says the floor of (the coe of) an integer is itself. Maybe floor_int would be a better name ? (Like the already-existing floor_add_int)
src/topology/algebra/floor_ring.lean
Outdated
| exact (lt_add_one _).le | ||
| end | ||
|
|
||
| lemma tendsto_floor_at_bot : |
There was a problem hiding this comment.
I'm sure all these lemmas name+statement will fit on one line after opening the filter namespace.
src/topology/algebra/floor_ring.lean
Outdated
| filter.tendsto (λ x, floor x : α → α) (𝓝[Ici n] n) (𝓝[Ici n] n) := | ||
| tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _ (tendsto_floor_right' _) | ||
| begin | ||
| refine (eventually_nhds_with_of_forall $ λ x (hx : ↑n ≤ x), _), |
There was a problem hiding this comment.
Is possible, please use type ascriptions instead of coercion arrows.
src/topology/algebra/floor_ring.lean
Outdated
|
|
||
| local notation `I` := (Icc 0 1 : set α) | ||
|
|
||
| lemma continuous_on.comp_fract {β : Type*} [order_topology α] |
There was a problem hiding this comment.
Did you try to deduce this lemma from the next one (with unit as a parameter space)? Or does it require so much plumbing that you don't gain anything?
PatrickMassot
added
awaiting-author
|
👎 Rejected by label |
github-actions
bot
added
the
ready-to-merge
|
@PatrickMassot Sorry I didn't think you would be so reactive, I just made a last small change in |
ADedecker
added
awaiting-review
|
bors merge |
github-actions
bot
added
ready-to-merge
…`floor`, `ceil` and `fract` (#4042) From the sphere eversion project
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
floor, ceil and fractfloor, ceil and fract
From the sphere eversion project
The four first lemma of
topology/algebra/floor_ringdon't need a topology but I'm not sure where to put them