exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le

English

If x ≤ y in α with LT and GT well-foundedness, there exists a finite chain x = a0 < a1 < ... < an = y where each step is a cover relation.

Русский

Если x ≤ y в α и выполняются условия LT и GT хорошо основанности, существует конечная цепь x = a0 < a1 < ... < an = y, каждая пара соединена соотношением покрытия.

LaTeX

$$$$\exists a:\mathbb{N} \to \alpha,\ a(0)=x \land \exists n, a(n)=y \land \forall i

Lean4

theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le {α : Type*} [PartialOrder α] [wfl : WellFoundedLT α]
    [wfg : WellFoundedGT α] {x y : α} (h : x ≤ y) : ∃ a : ℕ → α, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1) :=
  by
  let S := Set.Icc x y
  let hS : BoundedOrder S := { top := ⟨y, h, le_rfl⟩, le_top x := x.2.2, bot := ⟨x, le_rfl, h⟩, bot_le x := x.2.1 }
  obtain ⟨a, h₁, n, h₂, e⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT S
  simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂
  exact
    ⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦
      ⟨(e i hi).1, fun c hc h ↦ (e i hi).2 (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩

Похожие утверждения