English
DirectedOn (r on f) s is equivalent to DirectedOn r (Set.image f s).
Русский
DirectedOn (r on f) s эквивалентно DirectedOn r (Set.image f s).
LaTeX
$$$DirectedOn\\ (Function.onFun r f)\\ s \\iff DirectedOn\\ r\\ (Set.image f\\ s)$$$
Lean4
theorem directedOn_onFun_iff {r : α → α → Prop} {f : β → α} {s : Set β} :
DirectedOn (r on f) s ↔ DirectedOn r (f '' s) :=
by
refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩
obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y) (Set.mem_image_of_mem f hy)
grind