English
For a relation r on α and a function f: β → α and a set s ⊆ β, the directedness of r on the image f[s] is equivalent to the directedness of the pullback on s via f.
Русский
Для отношения r на α и функции f: β → α и множества s ⊆ β, направленность (DirectedOn) r на образ f[s] эквивалентна направленности на обратном образе через f.
LaTeX
$$$DirectedOn\\ r\\ (Set.image\\ f\\ s) \\iff DirectedOn\\ (Order.Preimage\\ f\\ r)\\ s$$$
Lean4
/-- A subset of α is directed if there is an element of the set `≼`-above any
pair of elements in the set. -/
def DirectedOn (s : Set α) :=
∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, x ≼ z ∧ y ≼ z
