worth copying defeq uIoc/uIcc lemmas?

Stream: new members

[llllvvuu]

import Mathlib.Data.Set.Intervals.UnorderedInterval

example {E : Type*} [LinearOrder E] {a b : E} : Set.uIoc a b ⊆ Set.uIcc a b := by
  -- exact? fails
  -- simp made no progress
  -- apply? returns junk
  exact Set.Ioc_subset_Icc_self -- succeeds

Should a copy of the Ioc/Icc API exist for uIoc/uIcc?

[Eric Wieser]

Yes, I think it should

[Eric Wieser]

I'm surprised that proof works

[Eric Wieser]

Either that, or we should make the u variants abbrevs

[Eric Wieser]

Maybe @Yaël Dillies has an opinion?

[Yaël Dillies]

My two (overly informed) cents:

• They should be abbrev on the basis that we use them relatively little and that there are many lemmas to copy
• They should not be abbrev for performance because a and b appear twice in their definition (uIcc a b = Icc (a ⊓ b) (a ⊔ b)