Set.uIxx

Stream: mathlib4

[Yury G. Kudryashov]

I have to unrelated questions about docs#Set.uIcc etc.

• We have notation for docs#Set.uIcc and docs#Set.uIoc but not for docs#Set.Icc etc. Do we really need this notation?
• I want to use Set.uIcc in file#Mathlib/Order/Interval/Set/Fin. Which option is better:
  • move them to Defs assuming Min and Max instead of Lattice?
  • move them to a new UnorderedDefs file while preserving the assumptions?
  • try to import UnorderedInterval and see how many transitive imports it adds to the closure?