Commit 2022-12-30 11:50 00088a48

View on Github →

chore: various naming fixes (#1258)

Estimated changes

deleted theorem Set.OrdConnected_Icc
deleted theorem Set.OrdConnected_Ici
deleted theorem Set.OrdConnected_Ico
deleted theorem Set.OrdConnected_Iic
deleted theorem Set.OrdConnected_Iio
deleted theorem Set.OrdConnected_Ioc
deleted theorem Set.OrdConnected_Ioi
deleted theorem Set.OrdConnected_Ioo
deleted theorem Set.OrdConnected_def
deleted theorem Set.OrdConnected_dual
deleted theorem Set.OrdConnected_empty
deleted theorem Set.OrdConnected_iff
deleted theorem Set.OrdConnected_image
deleted theorem Set.OrdConnected_interval
deleted theorem Set.OrdConnected_interᵢ
deleted theorem Set.OrdConnected_interₛ
deleted theorem Set.OrdConnected_of_Ioo
deleted theorem Set.OrdConnected_pi
deleted theorem Set.OrdConnected_preimage
deleted theorem Set.OrdConnected_range
deleted theorem Set.OrdConnected_univ
deleted theorem Set.dual_OrdConnected
deleted theorem Set.dual_OrdConnected_iff
added theorem Set.dual_ordConnected
added theorem Set.ordConnected_Icc
added theorem Set.ordConnected_Ici
added theorem Set.ordConnected_Ico
added theorem Set.ordConnected_Iic
added theorem Set.ordConnected_Iio
added theorem Set.ordConnected_Ioc
added theorem Set.ordConnected_Ioi
added theorem Set.ordConnected_Ioo
added theorem Set.ordConnected_def
added theorem Set.ordConnected_dual
added theorem Set.ordConnected_empty
added theorem Set.ordConnected_iff
added theorem Set.ordConnected_image
added theorem Set.ordConnected_pi
added theorem Set.ordConnected_range
added theorem Set.ordConnected_univ
added theorem isCompl_compl
deleted theorem is_compl_compl