OrdConnected class

Stream: mathlib4

[Violeta Hernández]

Might I ask why docs#Set.OrdConnected is registered as a class, rather than just a structure? In what kinds of situations do we want to be using typeclass inference with it?

[Yury G. Kudryashov]

I found these instances: docs#Set.instDenselyOrdered docs#ordConnectedSubsetConditionallyCompleteLinearOrder docs#Set.OrdConnected.isPredArchimedean docs#Set.OrdConnected.isSuccArchimedean docs#instIsStronglyAtomicElemOfOrdConnected docs#instIsStronglyCoatomicElemOfOrdConnected