sequentialFunctor_final_aux — Mathlib

English

For every j in J, there exists n with j ≤ sequentialFunctor_obj J n (cofinality of the sequence).

Русский

Для каждого j в J существует неотрицательное число n такое, что j ≤ sequentialFunctor_obj J n (свойство кофинитности последовательности).

LaTeX

$$$ \\exists n: \\mathbb{N},\\ j \\le \\text{sequentialFunctor\\_obj } J n $$$

Lean4

theorem sequentialFunctor_final_aux (j : J) : ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n :=
  by
  obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j
  refine ⟨m + 1, ?_⟩
  simpa only [h] using
    leOfHom
      (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose m)
          (sequentialFunctor_obj J m)).choose_spec.choose

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