Theorems · Theorem · order theory

DirectedOn.mono_comp

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α},
  (∀ ⦃x y : α⦄, r x y → rb (g x) (g y)) → DirectedOn r s → DirectedOn rb (g '' s)

Defined in

Mathlib.Order.Directed

Cited by

10 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext, Quot.sound