English
Equivalence between Directed on a function and DirectedOn on its range.
Русский
Эквивалентность между Directed на функции и DirectedOn на её диапазоне.
LaTeX
$$$Directed r f \\iff DirectedOn r (Set.range f)$$$
Lean4
theorem extend_bot [Preorder α] [OrderBot α] {e : ι → β} {f : ι → α} (hf : Directed (· ≤ ·) f)
(he : Function.Injective e) : Directed (· ≤ ·) (Function.extend e f ⊥) :=
by
intro a b
rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
· use b
simp [Function.extend_apply' _ _ _ ha]
rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
· use e i
simp [Function.extend_apply' _ _ _ hb]
rcases hf i j with ⟨k, hi, hj⟩
use e k
simp only [he.extend_apply, *, true_and]
