English
Given a finite subset S of α and a dense β with no endpoints, there exists an order-embedding extending an existing embedding f when inserting a point a not in S that preserves strict monotonicity.
Русский
Для непустого конечного подмножества S и плотного β без пределов существует вложение порядка, расширяющее заданное отображение f при вставке нового элемента a, сохраняя строгую монотонность.
LaTeX
$$$\\exists g : (insert a S) \\hookrightarrow_o β,\\; g \\circ (inclusion) = f$$$
Lean4
theorem exists_orderEmbedding_insert [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [nonem : Nonempty β]
(S : Finset α) (f : S ↪o β) (a : α) :
∃ (g : (insert a S : Finset α) ↪o β), g ∘ (Set.inclusion ((S.subset_insert a) : ↑S ⊆ ↑(insert a S))) = f :=
by
let Slt := {x ∈ S.attach | x.val < a}.image f
let Sgt := {x ∈ S.attach | a < x.val}.image f
obtain ⟨b, hb, hb'⟩ :=
Order.exists_between_finsets Slt Sgt
(fun x hx y hy =>
by
simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists, exists_and_left,
Slt, Sgt] at hx hy
obtain ⟨_, hx, _, rfl⟩ := hx
obtain ⟨_, hy, _, rfl⟩ := hy
exact f.strictMono (hx.trans hy))
refine
⟨OrderEmbedding.ofStrictMono (fun (x : (insert a S : Finset α)) => if hx : x.1 ∈ S then f ⟨x.1, hx⟩ else b) ?_, ?_⟩
· rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
if hxS : x ∈ S then
if hyS : y ∈ S then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
else
obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
simp only [hxS, hyS, ↓reduceDIte]
exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
else
obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
if hyS : y ∈ S then
simp only [hxS, hyS, ↓reduceDIte]
exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy
· ext x
simp only [OrderEmbedding.coe_ofStrictMono, Finset.insert_val, Function.comp_apply, Finset.coe_mem, ↓reduceDIte,
Subtype.coe_eta]
