Theorems · Theorem · order theory

RelHomClass.directedOn

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_3} [inst : FunLike F α β]
  [RelHomClass F r s] {f : F} {t : Set α}, DirectedOn r t → DirectedOn s (⇑f '' t)

Defined in

Mathlib.Order.RelIso.Set

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeRelHomClass