exists_small_weakly_initial_set — Mathlib

English

A technical matching lemma for the initiality of the inclusion of a full subcategory; relates costructured arrows and morphisms inside a discrete setup.

Русский

Техническая лемма согласования для начальности включения полной подсистемы; связывает CostructuredArrow и морфизмы в дискретной настройке.

LaTeX

$$$\\forall C, P, d,\\ motive, x,\\; \\dots$$$

Lean4

/-- The converse is true if `J` is cofiltered, see `initiallySmall_of_small_weakly_initial_set`. -/
theorem exists_small_weakly_initial_set [InitiallySmall.{w} J] :
    ∃ (s : Set J) (_ : Small.{w} s), ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i) :=
  by
  refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩
  obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty
  exact ⟨(fromInitialModel J).obj f.left, Set.mem_range_self _, ⟨f.hom⟩⟩

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