English
If s is directed with respect to r and a is added to s preserving reflexivity, and every b in s has a common upper bound with a, then insert a yields a directed set.
Русский
Если множество s направлено относительно r и к нему добавляется элемент a, сохраняется рефлексивность, и для каждого b в s существует общий верхний предел с a, то добавление a сохраняет направленность.
LaTeX
$$$\forall a, \text{DirectedOn}(r, S) \rightarrow \left(\forall b \in S, \exists c \in S, a \preceq c \land b \preceq c\right) \rightarrow \text{DirectedOn}(r, \text{insert}(a,S))$$$
Lean4
protected theorem insert (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s)
(ha : ∀ b ∈ s, ∃ c ∈ s, a ≼ c ∧ b ≼ c) : DirectedOn r (insert a s) :=
by
rintro x (rfl | hx) y (rfl | hy)
· exact ⟨y, Set.mem_insert _ _, h _, h _⟩
· obtain ⟨w, hws, hwr⟩ := ha y hy
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
· obtain ⟨w, hws, hwr⟩ := ha x hx
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
· obtain ⟨w, hws, hwr⟩ := hd x hx y hy
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
