English
If X is locally connected, there exists a bottom element in the order on DiscreteQuotient(X), given by the connected component setoid.
Русский
Если X локально связно, существует нижний элемент в порядке над DiscreteQuotient(X), задаваемый связной компонентой как эквивалентностью.
LaTeX
$$$$\\text{If } X \\text{ is locally connected, then } \\mathrm{DiscreteQuotient}(X) \\text{ has a bottom element } \\bot, \\text{ with } \\bot = \\text{connectedComponentSetoid}(X).$$$$
Lean4
/-- When `X` is a locally connected space, there is an `OrderBot` instance on
`DiscreteQuotient X`. The bottom element is given by `connectedComponentSetoid X`
-/
instance [LocallyConnectedSpace X] : OrderBot (DiscreteQuotient X)
where
bot :=
{ toSetoid := connectedComponentSetoid X
isOpen_setOf_rel := fun x => by
convert isOpen_connectedComponent (x := x)
ext y
simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using eq_comm }
bot_le
S := fun x y (h : connectedComponent x = connectedComponent y) =>
(S.isClopen_setOf_rel x).connectedComponent_subset (S.refl _) <| h.symm ▸ mem_connectedComponent
