English
If there exists a chain of a certain form on the restriction of a function f, then the induced order on the codomain is directed via f.
Русский
Если существует цепь определённой формы на ограничении функции f, то индуцированный порядок на кодомапа подвержен направленности через f.
LaTeX
$$$ (IsChain\\ (f^{-1} o r)\\ c) \\rightarrow DirectedOn\\ r\\ (f|_{c}) $$$
Lean4
protected theorem directed {f : β → α} {c : Set β} (h : IsChain (f ⁻¹'o r) c) :
Directed r fun x : { a : β // a ∈ c } => f x := fun ⟨a, ha⟩ ⟨b, hb⟩ =>
(by_cases fun hab : a = b => by
simp only [hab, exists_prop, and_self_iff, Subtype.exists]
exact ⟨b, hb, refl _⟩)
fun hab => ((h ha hb hab).elim fun h => ⟨⟨b, hb⟩, h, refl _⟩) fun h => ⟨⟨a, ha⟩, refl _, h⟩
