mathlib3
9003f287 - chore(data/set/intervals/unordered_interval): Rename to `uIcc`/`uIoc` (#18104)

Commit
2 years ago
chore(data/set/intervals/unordered_interval): Rename to `uIcc`/`uIoc` (#18104) Rename * `set.interval` → `set.uIcc` * `set.interval_oc` → `set.uIoc` * `finset.interval`→ `finset.uIcc` Closes #17982 Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Set.20intervals.20names
Author
Parents
Loading