initiallySmall_of_small_weakly_initial_set

English

If J is IsCofilteredOrEmpty and s is a small subset of J with hs(i) providing a map i ⟶ j for some j in s for each i, then InitiallySmall J.

Русский

Если J имеет свойство IsCofilteredOrEmpty и есть малый набор s с тем, что для каждого i существует j в s и i ⟶ j, то J является InitiallySmall.

LaTeX

$$$[\\text{IsCofilteredOrEmpty } J] \\Rightarrow [\\text{InitiallySmall } J]$ with $s$ and $hs$$$

Lean4

theorem initiallySmall_of_small_weakly_initial_set [IsCofilteredOrEmpty J] (s : Set J) [Small.{v} s]
    (hs : ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i)) : InitiallySmall.{v} J :=
  by
  suffices Functor.Initial (ObjectProperty.ι (· ∈ s)) from
    initiallySmall_of_initial_of_essentiallySmall (ObjectProperty.ι (· ∈ s))
  refine Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)
  obtain ⟨j, hj₁, hj₂⟩ := hs i
  exact ⟨⟨j, hj₁⟩, hj₂⟩

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