covBy_iff_lt_iff_le

Stream: Is there code for X?

[Violeta Hernández]

Do we by chance have something like this?

import Mathlib.Order.Cover

theorem covBy_iff_lt_iff_le [LinearOrder α] {x y : α} : x ⋖ y ↔ ∀ {z}, z < y ↔ z ≤ x where
  mp := fun hx _z ↦ ⟨hx.le_of_lt, fun hz ↦ hz.trans_lt hx.lt⟩
  mpr := fun H ↦ ⟨H.2 le_rfl, fun _z hx hz ↦ (H.1 hz).not_lt hx⟩

[Ruben Van de Velde]

@Yaël Dillies

[Yaël Dillies]

Not that I know of

[Violeta Hernández]

Alright, will PR later

[Eric Wieser]

The version with the relations swapped would be good to have too