∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {f g : α → β}
  {hf : ∀ (x : β), MeasurableSet (f ⁻¹' {x})} {hg : ∀ (x : β), MeasurableSet (g ⁻¹' {x})} {hf' : (Set.range f).Finite}
  {hg' : (Set.range g).Finite},
  { toFun := f, measurableSet_fiber' := hf, finite_range' := hf' } <
      { toFun := g, measurableSet_fiber' := hg, finite_range' := hg' } ↔
    f < g