UpperSets in LinearOrder

Stream: Is there code for X?

[Junyan Xu]

This is a pretty roundabout way to construct this quite intuitive OrderIso:

import Mathlib.Order.Birkhoff -- 460 imports
noncomputable def UpperSet.orderIsoWithTopOfFinite (α) [LinearOrder α] [Finite α] :
    UpperSet α ≃o WithTop α :=
  WithTop.subtypeOrderIso.symm.trans <| .withTopCongr <| .trans
    (.setCongr {⊤}ᶜ (setOf InfIrred) <| by ext; simp) <| .symm .infIrredUpperSet

The following is more straightforward and imports less (though not a subset of the implementation above):

import Mathlib.Data.Finset.Max
import Mathlib.Data.Set.Finite.Basic
import Mathlib.Order.UpperLower.Principal
#trans_imports "Mathlib." -- 394 imports

def UpperSet.equivWithTopOfFinite (α) [LinearOrder α] [Finite α] : UpperSet α ≃o WithTop α where
  toFun s := s.1.toFinite.toFinset.min
  invFun i := i.recTopCoe ⊤ .Ici
  left_inv s := by sorry
  right_inv i := i.recTopCoe (by simp) fun i ↦ (Finset.min_le (by simp)).antisymm (by simp)
  map_rel_iff' := sorry

If there is no better suggestion I'd stick with the first implementation.

[Aaron Liu]

I don't like UpperSet. Why are you using UpperSet?

[Junyan Xu]

Do you like LowerSet better? See #PR reviews > #25140 Hahn embedding theorem @ 💬 for the motivation.

[Aaron Liu]

well docs#upperSetIsoLowerSet, which is exactly why I don't like them (which one do you pick? there's no canonical choice)

[Aaron Liu]

would be better if they were paired

[Junyan Xu]

This is interesting, UpperSet α and LowerSet α are canonically isomorphic, but the embedding of α into them are not the same ...

[Aaron Liu]

maybe we can find out which one to use by thinking about what happens in a nonlinear order