mathlib

34c3668e - chore(data/set/intervals/ord_connected): make it more useful as a typeclass (#4879)

chore(data/set/intervals/ord_connected): make it more useful as a typeclass (#4879) * Add `protected lemma set.Icc_subset` that looks for `ord_connected s` instance. * Add `instance` versions to more lemmas. * Add `ord_connected_pi`.