directedOn_onFun_iff — Mathlib

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

Похожие утверждения