Commit 2024-06-07 23:31 3ee149ac

View on Github →

feat: Topological properties of order-connected sets in ℝⁿ (#10565) Partially forward-port https://github.com/leanprover-community/mathlib/pull/16976

Estimated changes

added theorem dist_anti_left_pi
added theorem dist_anti_right_pi
added theorem dist_inf_sup_pi
added theorem dist_le_dist_of_le_pi
added theorem dist_mono_left_pi
added theorem dist_mono_right_pi
modified theorem bddAbove_singleton
modified theorem bddBelow_singleton
added def orderBornology