General topology lemma (complement is connected)

Stream: Is there code for X?

[Béranger Seguin]

Hi everyone!

I needed the following lemma from general topology (see e.g., Kuratowski, Introduction to Set Theory and Topology, Chap. XVI, §3, Theorem 4): if X is connected, A⊆X is connected, C is a connected component of X∖A, then X∖C is connected. I wrote a ≈150lines proof of this (this is AxiomC3_general in this code).

Is this lemma actually somewhere in mathlib, to avoid me proving it? Should it? It is important enough that it is one of the four properties of connected sets retained in this axiomatisation of the notion (property (iv) is equivalent to this, cf. top of page 4).

Thanks to everybody! And I'm always happy to hear about ways to write my proofs in a more canonical/idiomatic way :-)
Béranger

[Vlad Tsyrklevich]

Do you know about grind? You are doing a fair number of things manually that grind can help with, e.g. your wlog statements and some intermediate statement like MUNVdisj are handled by a single call to grind

[Vlad Tsyrklevich]

Small style comments, instead of by apply I'd just give a term, e.g.
have CinXmA : C ⊆ X \ A := connectedComponentIn_subset _ _
have yinC : y ∈ C := mem_connectedComponentIn ynotinA

Use exact instead of apply when it closes the goal

Instead of

    by_contra UVdisj
    rw [not_nonempty_iff_eq_empty] at UVdisj

Use

    by_contra! UVdisj

to simplify the negation at once

There is something called dot notaiton, instead of IsOpen.union Mopen Uopen you can make it shorter by writing Mopen.union Uopen since Mopen is of type IsOpen.

[Vlad Tsyrklevich]

For selecting an implication of an Iff, prefer using the names .mp and .mpr instead of .1 and .2

[Vlad Tsyrklevich]

Instead of a series of applys/intros, you can often merge these into a single refine statement. Especially as a beginner I found these refines in mathlib a bit hard to read, but once you have done some golfing of your own proofs and combining consecutive applys intro refines, you will find them more concise and therefore readable

[Vlad Tsyrklevich]

I have not tried to golf the first proof much, and I could probably go further with the second proof but I think this is enough to show you some new ideas

import Mathlib.Topology.Connected.Basic
import Mathlib.Data.Set.Basic

open Set
--- Béranger Seguin
--- Lean 4.25 (2025-11-30, updated 2025-12-07)
--- Formalization of results from "Flimsy Spaces" (arXiv:2511.17745)

universe u
variable {α : Type u} [TopologicalSpace α]

theorem ConnectedInSeparated
  {A U V : Set α}
  (connA : IsPreconnected A)
  (Uopen : IsOpen U) (Vopen : IsOpen V)
  (UVdisj : A ∩ (U ∩ V) = ∅) (UVcover : A ⊆ U ∪ V)
  : A ⊆ U ∨ A ⊆ V
  := by
    by_contra h
    apply nonempty_iff_ne_empty.1 _ UVdisj
    apply connA U V Uopen Vopen UVcover
    all_goals by_contra disj
    all_goals apply h
    on_goal 1 => right
    on_goal 2 => left
    all_goals intro a ha
    all_goals have notin := eq_empty_iff_forall_notMem.1 (not_nonempty_iff_eq_empty.1 disj) a
    all_goals grind

theorem AxiomC3_general
  --- Kuratowski (Introduction to Set Theory and Topology), Chap. XVI, §3, Theorem 4
  {X A : Set α}
  (connX : IsPreconnected X)
  (connA : IsPreconnected A) (AinX : A ⊆ X)
  (y : α) (ynotinA : y ∈ X \ A)
  : IsPreconnected (X \ (connectedComponentIn (X \ A) y))
  := by
    set C := (connectedComponentIn (X \ A) y)

    --- Write X \ C = (U ∪ V) ∩ (X \ C) for two opens U, V meeting (X \ C)
    intro U V Uopen Vopen UVcover Unonempty Vnonempty
    --- Assume by contradiction that U ∩ V ∩ (X \ C) = ∅
    by_contra! UVdisj

    have CinXmA : C ⊆ X \ A := connectedComponentIn_subset _ _
    --- A is connected and ⊆ U ∪ V, so is contained in either U or V
    have AUVdisj : A ∩ (U ∩ V) = ∅ := by grind
    have AinUorV :=
      ConnectedInSeparated connA Uopen Vopen AUVdisj (subset_trans (by grind) UVcover)

    --- Without loss of generality A ⊆ U
    wlog AinU : A ⊆ U generalizing U V
    · grind

    have yinC : y ∈ C := mem_connectedComponentIn ynotinA

    --- If we show that C ∪ (V ∩ X) is connected, then we are done:
    --- Indeed: by maximality of C, this implies V∩X⊆C, i.e., V∩(X\C) = ∅
    suffices connCV : IsPreconnected (C ∪ (V ∩ X)) by
      refine nonempty_iff_ne_empty.mp Vnonempty <|
        eq_empty_iff_forall_notMem.mpr (fun x ⟨⟨inX, notinC⟩, inV⟩ ↦ notinC ?_)
      refine mem_of_subset_of_mem (s₁ := C ∪ V ∩ X) ?_ (Or.inr ⟨ inV, inX ⟩)
      apply IsPreconnected.subset_connectedComponentIn connCV (Or.inl yinC)
      simp [CinXmA]
      intro v ⟨ inV, inX ⟩
      grind [eq_empty_iff_forall_notMem.1 AUVdisj v]

    --- To show that C ∪ (V ∩ X) is connected, we assume that it is covered by two opens M and N
    --- which meet it and are disjoint within it
    intro M N Mopen Nopen MNcover Mnonempty Nnonempty
    by_contra! MNdisj

    --- C connected ⊆ M ∪ N so C is contained in either
    have CinMorN : C ⊆ M ∨ C ⊆ N := by
      apply ConnectedInSeparated (isPreconnected_connectedComponentIn) Mopen Nopen <;> grind

    --- Without loss of generality, C ⊆ M and then C ∩ N = ∅
    wlog CinM : C ⊆ M generalizing M N
    · grind
    have CNdisj : C ∩ N = ∅ := by
      grind
    suffices CVXNdisj : (C∪(V∩X)) ∩ N = ∅ by
      grind [nonempty_iff_ne_empty]

    simp [union_inter_distrib_right, CNdisj]
    have MUNVcover : X ⊆ (M ∪ U) ∪ (N ∩ V) := by
      intro x inX
      by_cases inM : x ∈ M
      · simp [inM]
      · have inUV : x ∈ U ∪ V := by grind
        rcases inUV with inU|inV
        · exact Or.inl (Or.inr inU)
        · have := MNcover (Or.inr ⟨ inV, inX ⟩)
          grind
    have XinMUorNV : X ⊆ M ∪ U ∨ X ⊆ N ∩ V :=
      ConnectedInSeparated connX (Mopen.union Uopen) (Nopen.inter Vopen) (by grind) MUNVcover
    have MUXnonempty : (M ∪ U) ∩ X ≠ ∅ := nonempty_iff_ne_empty.mp ⟨y, by grind⟩
    grind

[Vlad Tsyrklevich]

Note in some places I use some syntax like <| where a <| b <| c <| <| d <| e is syntax sugar for a (b (c (d e))) but avoids all the nested parentheses. This is one of those things that I found a bit confusing bit earlier but once you use it a bit yourself you see that it really reduces parentheses and makes proofs more readable.

[Vlad Tsyrklevich]

I have focused solely on golfing downing the proof, I have not looked at the contents of the proof or to see if any improvements may be made by using mathlib itself more.

[Béranger Seguin]

This is incredible! I indeed did not know about grind. Almost feels like cheating!
I updated my code using some of your recommandations.

[Snir Broshi]

Tried to shorten your updated code further:

import Mathlib.Topology.Connected.Basic
import Mathlib.Data.Set.Basic

open Set

variable {α : Type*} [TopologicalSpace α]

theorem ConnectedInSeparated {A U V : Set α} (connA : IsPreconnected A) (Uopen : IsOpen U)
    (Vopen : IsOpen V) (UVdisj : Disjoint A (U ∩ V)) (UVcover : A ⊆ U ∪ V) : A ⊆ U ∨ A ⊆ V := by
  by_contra!
  apply nonempty_iff_ne_empty.mp _ <| disjoint_iff_inter_eq_empty.mp UVdisj
  apply connA U V Uopen Vopen UVcover
  all_goals by_contra!
  · grind [Disjoint.subset_right_of_subset_union, disjoint_iff_inter_eq_empty]
  · grind [Disjoint.subset_left_of_subset_union, disjoint_iff_inter_eq_empty]

theorem AxiomC3_general {X A : Set α} (y : α) (connX : IsPreconnected X) (connA : IsPreconnected A)
    (AinX : A ⊆ X) : IsPreconnected <| X \ (connectedComponentIn (X \ A) y) := by
  by_cases! y ∉ X \ A
  · grind [connectedComponentIn_eq_empty, diff_empty]
  set C := connectedComponentIn (X \ A) y
  intro U V Uopen Vopen UVcover Unonempty Vnonempty
  by_contra! UVdisj
  have AinUorV : A ⊆ U ∨ A ⊆ V := by
    apply ConnectedInSeparated <;> grind [connectedComponentIn_subset, disjoint_iff_inter_eq_empty]
  wlog AinU : A ⊆ U generalizing U V
  · grind
  suffices connCV : IsPreconnected (C ∪ (V ∩ X)) by
    apply nonempty_iff_ne_empty.mp Vnonempty <| eq_empty_iff_forall_notMem.mpr _
    grind [mem_of_subset_of_mem (s₁ := C ∪ V ∩ X), IsPreconnected.subset_connectedComponentIn,
      connectedComponentIn_subset, mem_connectedComponentIn, subset_diff, disjoint_union_left,
      disjoint_iff_inter_eq_empty]
  intro M N Mopen Nopen MNcover
  by_contra!
  have CinMorN : C ⊆ M ∨ C ⊆ N := by
    apply ConnectedInSeparated <;>
      grind [isPreconnected_connectedComponentIn, disjoint_iff_inter_eq_empty]
  wlog CinM : C ⊆ M generalizing M N
  · grind
  have MUNVcover : X ⊆ (M ∪ U) ∪ (N ∩ V) := by
    intro x inX
    by_cases x ∈ M
    · grind
    · obtain inU | inV : x ∈ U ∪ V := by grind
      · grind
      · have := MNcover <| .inr ⟨inV, inX⟩
        grind
  have := ConnectedInSeparated connX (Mopen.union Uopen) (Nopen.inter Vopen)
  grind [disjoint_iff_inter_eq_empty, nonempty_iff_ne_empty]