some pointset topology

Stream: condensed mathematics

[Adam Topaz]

In case anyone is bored and wants to tackle some pointset topology, there are three sorry's in the file for_mathlib/Profinite/disjoint_union.lean that are very doable (with no category theory :wink: ):

instance {α : Type*} [fintype α] (X : α → Type*) [∀ a, topological_space (X a)]
  [∀ a, compact_space (X a)] : compact_space (Σ a, X a) := sorry

instance {α : Type*} [fintype α] (X : α → Type*) [∀ a, topological_space (X a)]
  [∀ a, totally_disconnected_space (X a)] : totally_disconnected_space (Σ a, X a) := sorry

instance {X Y : Type*} [topological_space X] [topological_space Y]
  [totally_disconnected_space X] [totally_disconnected_space Y] :
  totally_disconnected_space (X ⊕ Y) := sorry

[Yaël Dillies]

That might be a good way to exercise my current Analysis & Topology lectures!

[Adam Topaz]

(The fintype assumption can be removed for the second sorry)

[Reid Barton]

The first one is basically docs#compact_Union

[Yaël Dillies]

May I get write access?

[Johan Commelin]

@Yaël Dillies https://github.com/leanprover-community/lean-liquid/invitations

[Yaël Dillies]

Thanks!

[Yaël Dillies]

Should I push to master or to a branch?

[Johan Commelin]

Feel free to push to master directly

[Yaël Dillies]

PRed in #10511

[Johan Commelin]

merci!