Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-03 15:50 34c3668e

View on Github →

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.

Estimated changes

modified theorem set.ord_connected_Icc
modified theorem set.ord_connected_Ici
modified theorem set.ord_connected_Ico
modified theorem set.ord_connected_Iic
modified theorem set.ord_connected_Iio
modified theorem set.ord_connected_Ioc
modified theorem set.ord_connected_Ioi
modified theorem set.ord_connected_Ioo
modified theorem set.ord_connected_empty
modified theorem set.ord_connected_interval
added theorem set.ord_connected_pi
modified theorem set.ord_connected_singleton
modified theorem set.ord_connected_univ