lt on functions

Stream: Is there code for X?

[Eric Wieser]

Does this exist somewhere?

lemma pi.lt_of_le_of_lt {α : Type*} {β : Type*} [preorder β]
  {f g : α → β} (h : f ≤ g) {x : α} (hx : f x < g x) : f < g :=
begin
  apply lt_of_le_not_le (pi.le_def.mpr h),
  rw [pi.le_def, not_forall],
  refine ⟨x, hx.not_le⟩,
end

[Eric Wieser]

Done in #6023