exists_orderEmbedding_covby_of_forall_covby_finite_of_bot

English

A constructive Krull-like lemma: given a structured system of finite projections and nonempty fibers, one can build a coherent sequence via a choice of compatible elements.

Русский

Конструктивная лемма, аналог Кёрла: при задании системы проекцияций с конечными волокнами и непустыми фибрами можно построить последовательность согласованных элементов.

LaTeX

$$$\\exists f : (i:\\mathbb{N}) \\to \\alpha_i, \\forall i \\le j, \\pi_{i j}(f(j)) = f(i).$$$

Lean4

/-- A version of Kőnig's lemma where the sequence starts at the minimum of an infinite order. -/
theorem exists_orderEmbedding_covby_of_forall_covby_finite_of_bot [OrderBot α] [Infinite α]
    (hfin : ∀ (a : α), {x | a ⋖ x}.Finite) : ∃ f : ℕ ↪o α, f 0 = ⊥ ∧ ∀ i, f i ⋖ f (i + 1) :=
  exists_orderEmbedding_covby_of_forall_covby_finite hfin (by simpa using infinite_univ)

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