exists_covBy_seq_of_wellFoundedLT_wellFoundedGT

English

Under LT and GT well-foundedness, there exists a sequence a: ℕ → α, starting from a minimal element, reaching a maximal element after finitely many steps, with each step being a cover relation.

Русский

При наличии хорошо основанных LT и GT существует последовательность a: ℕ → α, начинающаяся с минимального элемента, достигающая максимального после конечного числа шагов, где каждый переход является покрытием.

LaTeX

$$$$\exists a:\mathbb{N} \to \alpha,\ IsMin(a(0)) \land \exists n,\ IsMax(a(n)) \land \forall i

Lean4

theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α] [Nonempty α] [wfl : WellFoundedLT α]
    [wfg : WellFoundedGT α] : ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1) :=
  by
  choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
  have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
  classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ hα trivial, ?_⟩
  have cov n (hn : ¬IsMax (a n)) : a n ⋖ a (n + 1) :=
    by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ fun h' ↦ wellFounded_lt.not_lt_min _ H h' h⟩

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