[Merged by Bors] - chore(analysis/convex/topology): split #18187
Conversation
hrmacbeth
added
the
awaiting-CI
github-actions
bot
removed
the
awaiting-CI
hrmacbeth
added
the
awaiting-review
| /-- The set of vectors in the same ray as `x` is connected. -/ | ||
| lemma is_connected_set_of_same_ray (x : E) : is_connected {y | same_ray ℝ x y} := | ||
| begin | ||
| by_cases hx : x = 0, { simpa [hx] using is_connected_univ }, | ||
| simp_rw ←exists_nonneg_left_iff_same_ray hx, | ||
| exact is_connected_Ici.image _ ((continuous_id.smul continuous_const).continuous_on) | ||
| end | ||
|
|
||
| /-- The set of nonzero vectors in the same ray as the nonzero vector `x` is connected. -/ | ||
| lemma is_connected_set_of_same_ray_and_ne_zero {x : E} (hx : x ≠ 0) : | ||
| is_connected {y | same_ray ℝ x y ∧ y ≠ 0} := | ||
| begin | ||
| simp_rw ←exists_pos_left_iff_same_ray_and_ne_zero hx, | ||
| exact is_connected_Ioi.image _ ((continuous_id.smul continuous_const).continuous_on) | ||
| end |
There was a problem hiding this comment.
Although I originally proved these in a normed context, they should work in a more general topological context (with haveI : path_connected_space E := topological_add_group.path_connected, added to the first proof so that is_connected_univ works), without actually needing norms.
| import analysis.convex.topology | ||
| import analysis.convex.normed |
There was a problem hiding this comment.
I have some unfinished changes to make the topological lemmas in this file work for a general real topological vector space without requiring norms. My notes say the missing piece was an instance to deduce has_continuous_vadd for an affine subspace from has_continuous_vadd for the whole space (which should be straightforward, though I'm not sure where such an instance should go).
There was a problem hiding this comment.
I.e. I had [add_comm_group V] [module ℝ V] [topological_space V] [topological_add_group V] [has_continuous_smul ℝ V] [add_torsor V P] [topological_space P] [has_continuous_vadd V P] {s : affine_subspace ℝ P} and needed an instance for has_continuous_vadd s.direction s.
|
@jsm28 Do you mind if I do the split now, then you move the lemmas at the time when you generalize their context? |
|
I think doing the split now without generalizing the lemmas is fine. |
|
ok, let's do the split now and refactor later. A pure split is always easier to review than a split mixed with changes. |
github-actions
bot
added
ready-to-merge
Split the facts about the topology of convex sets into two files, for topological vector spaces and normed spaces. This makes the former a more elementary file, as indeed it feels like it should be. It also slightly decreases the length of the longest path in mathlib.
|
Build failed (retrying...): |
Split the facts about the topology of convex sets into two files, for topological vector spaces and normed spaces. This makes the former a more elementary file, as indeed it feels like it should be. It also slightly decreases the length of the longest path in mathlib.
|
Build failed (retrying...): |
|
I believe that bors failures are because of this PR (in the latest failed batch, there were 2 PRs, and the other one doesn't change |
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Canceled. |
github-actions
bot
added
the
delegated
|
bors r+ |
Split the facts about the topology of convex sets into two files, for topological vector spaces and normed spaces. This makes the former a more elementary file, as indeed it feels like it should be. It also slightly decreases the length of the longest path in mathlib.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Split the facts about the topology of convex sets into two files, for topological vector spaces and normed spaces. This makes the former a more elementary file, as indeed it feels like it should be. It also slightly decreases the length of the longest path in mathlib.