[Merged by Bors] - feat(data/set/basic, topology/{subset_properties, connected}): A space is preconnected iff every continuous map to a discrete space is constant #17070
Conversation
dagurtomas
added
awaiting-review
dagurtomas
changed the title
src/topology/connected.lean
Outdated
|
|
||
| /-- A set `s` is preconnected if and only if every | ||
| map into `bool` that is continuous on `s` is constant on `s` -/ | ||
|
|
There was a problem hiding this comment.
This blank line should be removed.
There was a problem hiding this comment.
Done. Also fixed the style errors that linter complained about.
leanprover-community-bot-assistant
added
ready-to-merge
|
Build failed: |
|
bors r- |
|
bors r+ |
|
bors r- |
|
Canceled. |
src/topology/connected.lean
Outdated
| /-- A set `s` is preconnected if and only if every | ||
| map into `bool` that is continuous on `s` is constant on `s` -/ |
There was a problem hiding this comment.
The docstring does not correspond to the content of the lemma. Docstrings appear as documentation attached to one single lemma, so you should give a docstring for this lemma adapated to its content, and another docstring for the next lemma.
YaelDillies
changed the title
| s.bool_indicator ⁻¹' t = sᶜ ∨ s.bool_indicator ⁻¹' t = ∅ := | ||
| begin | ||
| simp only [preimage_bool_indicator_eq_union], | ||
| split_ifs ; simp [s.union_compl_self] |
There was a problem hiding this comment.
| split_ifs ; simp [s.union_compl_self] | |
| split_ifs; simp [s.union_compl_self] |
| /-- If every map to `bool` (a discrete two-element space), that is | ||
| continuous on a set `s`, is constant on s, then s is preconnected -/ | ||
| lemma is_preconnected_of_forall_constant {s : set α} | ||
| (hs : ∀ f : α → bool, continuous_on f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : is_preconnected s := |
There was a problem hiding this comment.
Can you state this for all nontrivial spaces with the discrete topology, rather than just bool?
There was a problem hiding this comment.
I think it can even be generalized to any space that is not preconnected. But bool is the simplest such space so it's nice to state the result using it. The general proof pretty much reduces to the bool case (pick one point in a clopen set and one point outside of it, then the subspace of these two points is homeomorphic to bool).
| /-- `bool_indicator` maps `x` to `tt` if `x ∈ s`, else to `ff` -/ | ||
| noncomputable def bool_indicator (x : α) := | ||
| @ite _ (x ∈ s) (classical.prop_decidable _) tt ff |
There was a problem hiding this comment.
Once you generalise according to my previous comment, you won't need this anymore.
There was a problem hiding this comment.
Because bool is the simplest non-preconnected space, having an indicator function valued in bool is convenient. I thought about making a local has_zero bool instance and define bool_indicator in terms of set.indicator, or at least deduce lemmas from the set.indicator counterparts to reduces duplication, but it seems not many of them can be easily deduced, and the API for bool_indicator is sufficiently distinct from set.indicator to deserve a separate declaration. So I'm satisfied with the current situation.
|
bors merge |
…ce is preconnected iff every continuous map to a discrete space is constant (#17070) This useful characterisation was missing from mathlib. Co-authored-by: Patrick Massot <patrick.massot@math.cnrs.fr>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
|
What about my comments? 😢 |
eric-wieser
added
the
hacktoberfest-accepted
This useful characterisation was missing from mathlib.
Co-authored-by: Patrick Massot patrick.massot@math.cnrs.fr
Closes #16974 by completely redoing it as suggested by Patrick Massot.