Commit 2024-11-15 14:42 f9aff52f

View on Github →

feat: uIoo (#19050) This PR is the first in a series which breaks #9598 (proving that holomorphic functions on disks have primitives) into smaller pieces. This piece introduces the notation uIoo (unordered Interval, open-open) which is the oo analog of uIcc. Then we prove the analogous API theorems to those available for uIcc.

Estimated changes

added theorem Set.Ioo_min_max
added theorem Set.Ioo_subset_uIoo'
added theorem Set.Ioo_subset_uIoo
added theorem Set.dual_uIoo
added theorem Set.mem_uIoo_of_gt
added theorem Set.mem_uIoo_of_lt
added def Set.uIoo
added theorem Set.uIoo_comm
added theorem Set.uIoo_of_ge
added theorem Set.uIoo_of_gt
added theorem Set.uIoo_of_le
added theorem Set.uIoo_of_lt
added theorem Set.uIoo_of_not_ge
added theorem Set.uIoo_of_not_le
added theorem Set.uIoo_self
added theorem Set.uIoo_subset_uIcc