English
For a densely ordered codomain β with no minimum or maximum and nonempty β, and any partial iso f: α ⇀ β and any a ∈ α, there exists b ∈ β such that for every p in the graph of f, the relative order between p.fst and a equals the relative order between p.snd and b.
Русский
Пусть β плотно упорядочен и не имеет минимального и максимального элементов, β непусто; для any частичного изоморфизма f: α ⇀ β и любого a ∈ α существует b ∈ β, такой что для каждого p в графе f отношение между p.fst и a совпадает с отношением между p.snd и b.
LaTeX
$$$\\\\exists b \\\\in \\\\beta, \\\\forall p \\\\in f.\\\\val, \\\\operatorname{cmp}(\\\\operatorname{fst} p, a) = \\\\operatorname{cmp}(\\\\operatorname{snd} p, b).$$$
Lean4
/-- For each `a`, we can find a `b` in the codomain, such that `a`'s relation to
the domain of `f` is `b`'s relation to the image of `f`.
Thus, if `a` is not already in `f`, then we can extend `f` by sending `a` to `b`.
-/
theorem exists_across [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (f : PartialIso α β) (a : α) :
∃ b : β, ∀ p ∈ f.val, cmp (Prod.fst p) a = cmp (Prod.snd p) b :=
by
by_cases h : ∃ b, (a, b) ∈ f.val
· obtain ⟨b, hb⟩ := h
exact ⟨b, fun p hp ↦ f.prop _ hp _ hb⟩
have : ∀ x ∈ {p ∈ f.val | p.fst < a}.image Prod.snd, ∀ y ∈ {p ∈ f.val | a < p.fst}.image Prod.snd, x < y :=
by
intro x hx y hy
rw [Finset.mem_image] at hx hy
rcases hx with ⟨p, hp1, rfl⟩
rcases hy with ⟨q, hq1, rfl⟩
rw [Finset.mem_filter] at hp1 hq1
rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
exact lt_trans hp1.right hq1.right
obtain ⟨b, hb⟩ := exists_between_finsets _ _ this
use b
rintro ⟨p1, p2⟩ hp
have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩
rcases lt_or_gt_of_ne this with hl | hr
· have : p1 < a ∧ p2 < b := ⟨hl, hb.1 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hl⟩, rfl⟩)⟩
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this
exact this.1.trans this.2.symm
· have : a < p1 ∧ b < p2 := ⟨hr, hb.2 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hr⟩, rfl⟩)⟩
rw [← cmp_eq_gt_iff, ← cmp_eq_gt_iff] at this
exact this.1.trans this.2.symm
