feat(topology): prove a space is preconnected iff every continuous ma…

[dagurtomas]

…p to a discrete space is constant

this useful characterisation of connectedness was missing from mathlib.

---

[alreadydone]

Thanks for the PR! I'll look at the proofs later if no one beats me to it :)

[PatrickMassot]

Thank you very much for this first contribution! I let detailed comments in the beginning, but at some point the only efficient thing to do is to redo everything. I still hope you'll learn stuff from reading this after making your own version.

My first advice is to take seriously the fact that you want a bool-valued indicator function. So I created one, without relying on set.indicator because I didn't want to drag in all the dependencies of that function. You get:

open bool

namespace set
variables {α : Type*} (s : set α)

def bool_indicator (x : α) := 
@ite _ (x ∈ s) (classical.prop_decidable _) tt ff

lemma mem_iff_bool_indicator (x : α) : x ∈ s ↔ s.bool_indicator x = tt :=
by { unfold bool_indicator, split_ifs ; tauto }

lemma not_mem_iff_bool_indicator (x : α) : x ∉ s ↔ s.bool_indicator x = ff :=
by { unfold bool_indicator, split_ifs ; tauto }

lemma preimage_bool_indicator_tt : s.bool_indicator ⁻¹' {tt} = s :=
ext (λ α, (s.mem_iff_bool_indicator α).symm)

lemma preimage_bool_indicator_ff : s.bool_indicator ⁻¹' {ff} = sᶜ :=
ext (λ α, (s.not_mem_iff_bool_indicator α).symm)

open_locale classical

lemma preimage_bool_indicator_eq_union (t : set bool) :
  s.bool_indicator ⁻¹' t = (if tt ∈ t then s else ∅) ∪ (if ff ∈ t then sᶜ else ∅) :=
begin
  ext α,
  dsimp [bool_indicator],
  split_ifs ; tauto
end

lemma preimage_bool_indicator (t : set bool) :
  s.bool_indicator ⁻¹' t = univ ∨ s.bool_indicator ⁻¹' t = s ∨ 
  s.bool_indicator ⁻¹' t = sᶜ ∨ s.bool_indicator ⁻¹' t = ∅ :=
begin
  simp only [preimage_bool_indicator_eq_union],
  split_ifs ; simp [s.union_compl_self]
end

end set

to put somewhere in data.set.basic or a new file in the data.set folder. Also in data.set.basic we can add:

lemma preimage_subtype_coe_eq_compl {α : Type*} {s u v : set α} (hsuv : s ⊆ u ∪ v)
  (H : s ∩ (u ∩ v) = ∅) : (coe : s → α) ⁻¹' u = (coe ⁻¹' v)ᶜ :=
begin
  ext ⟨x, x_in_s⟩,
  split,
  { intros x_in_u x_in_v,
    exact eq_empty_iff_forall_not_mem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩ },
  { intro hx,
    exact or.elim (hsuv x_in_s) id (λ hx', hx.elim hx') }
end

Note that nothing above has anything to do with topology, so it definitely shouldn't be anywhere near the topology folder.

Inside the topology folder, next to the definition of clopen sets, you can put

variables {X : Type*} [topological_space X]

lemma continuous_bool_indicator_iff_clopen (U : set X) :
  continuous U.bool_indicator ↔ is_clopen U :=
begin
  split,
  { intros hc,
    rw ← U.preimage_bool_indicator_tt,
    exact ⟨hc.is_open_preimage _ trivial, continuous_iff_is_closed.mp hc _ (is_closed_discrete _)⟩ },
  { refine λ hU, ⟨λ s hs, _⟩,
    rcases U.preimage_bool_indicator s with (h|h|h|h) ; rw h,
    exacts [is_open_univ, hU.1, hU.2.is_open_compl, is_open_empty] },
end

lemma continuous_on_indicator_iff_clopen (s U : set X) :
  continuous_on U.bool_indicator s ↔ is_clopen ((coe : s → X) ⁻¹' U) :=
begin
  rw [continuous_on_iff_continuous_restrict, ← continuous_bool_indicator_iff_clopen],
  refl
end

All this is nice and useful and has nothing to do with connected sets. We've been doing what is called "filling API holes before tackling the stuff you actually care about". Note that some lemmas above won't be used in our main target, but they are expected once you define set.bool_indicator for instance. Now we can move to the file defining connected set, and we no longer need to create a new file there. First one implication is essentially already there, so let's simply state it.

lemma is_preconnected.constant {Y : Type*} [topological_space Y] [discrete_topology Y]
  {s : set X} (hs : is_preconnected s) {f : X → Y} (hf : continuous_on f s) 
  {x y : X} (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
(hs.image f hf).subsingleton (mem_image_of_mem f hx) (mem_image_of_mem f hy)

The converse implication is where we'll need the preliminaries.

lemma is_preconnected_of_forall_constant {s : set X} 
  (hs : ∀ f : X → bool, continuous_on f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : is_preconnected s := 
begin
  unfold is_preconnected,
  by_contra',
  rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩,
  rw [not_nonempty_iff_eq_empty] at H,
  have hy : y ∉ u,
    from λ y_in_u, eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩,
  have : continuous_on u.bool_indicator s,
  { apply (continuous_on_indicator_iff_clopen _ _).mpr ⟨_, _⟩,
    { exact continuous_subtype_coe.is_open_preimage u u_op },
    { rw preimage_subtype_coe_eq_compl hsuv H,
      exact (continuous_subtype_coe.is_open_preimage v v_op).is_closed_compl } },
  simpa [(u.mem_iff_bool_indicator _).mp x_in_u, (u.not_mem_iff_bool_indicator _).mp hy] using 
    hs _ this x x_in_s y y_in_s
end

Then you need to add a version for preconnected_space.

Thanks again for you contribution and I hope you'll learn some interesting stuff from this review!

[PatrickMassot]

This is function.const X tt.

[PatrickMassot]

Why did you feel you need that less general version? Does anything break if you replace all uses of cst_top' with cst_top?

[PatrickMassot]

For such statements that intuitively require no proof at all, the tradition is to compress the proof. Here you can write the exact same proof as

⟨λ hx, set.indicator_of_mem hx _, 
 λ hx, set.mem_of_indicator_ne_zero 
   (hx.symm ▸ (dec_trivial : ⊤ ≠ (0 : bool)) : U.indicator (cst_top X) x ≠ 0)⟩

(without begin and end, this is a proof term). For readers this is a clear indication that they don't want to see this proof.

[PatrickMassot]

You should never let such a line in a finished proof that needs to be maintainable. If someone adds a lemma to the simp set then the behavior of this line will change and the remaining part of the proof will be broken in a way that will be very difficult to diagnose. In this specific case, that line also does nothing at all in your proof.

[PatrickMassot]

This line isn't used at all. It's fine for exploration, but you need to cleanup before opening a PR.

[PatrickMassot]

This definition is a bad idea because it won't play well with the rest of mathlib.

[PatrickMassot]

This swap shouldn't stay in the final proof since it was only a psychological help for you.

[PatrickMassot]

It's better to avoid letting such an expensive tactic when a faster one would do the job. You could replace this proof with

⟨λ h, ⟨by tauto⟩, λ hf s, continuous_def.mp hf s (is_open_discrete s)⟩

for instance. Better, you could replace by tauto with λ s _, h s which is the actual proof (you can even use show_term to get that proof term).

[PatrickMassot]

Introducing this definition to use it only twice is a bad idea. Either you really need a definition and you need to prove a bunch of basic lemmas about it to make it useful or you don't need it.

Everything below this point starts being really suboptimal, and I think it's more efficient to show you how to do it in a more efficient way.

[PatrickMassot]

[decidable_pred (∈ α)] shouldn't be in the statement since it is not needed to state the lemma. You can remove it and start the proof with classical.

[dagurtomas]

Thank you for your detailed feedback, Patrick! It is certainly very helpful and I'm sure I'll learn a lot from it. I'll try to change the PR according to your suggestions.

[dagurtomas]

I've created a new PR #17070 which completely redoes this as Patrick suggests. Closing this one now.