A RelHom preserves DirectedOn

Stream: Is there code for X?

[Etienne Marion]

Is this statement missing? Do we want it in Mathlib? It seems useful to me.

import Mathlib

example {α β : Type*} {r : α → α → Prop} {s : β → β → Prop} (f : RelHom r s)
    {t : Set α} (hs : DirectedOn r t) : DirectedOn s (f '' t) := by
  rintro - ⟨a, ha, rfl⟩ - ⟨a', ha', rfl⟩
  obtain ⟨x, x_in, hx1, hx2⟩ := hs a ha a' ha'
  exact ⟨f x, ⟨x, x_in, rfl⟩, f.map_rel hx1, f.map_rel hx2⟩

Also I could not find anything which relates Monotone and RelHom other than docs#RelEmbedding.ofMonotone, but it's only for embeddings.

[Ruben Van de Velde]

I'd say yes, but maybe stated about RelHomClass

[Etienne Marion]

Thanks! I opened #20080