exists_small_weakly_terminal_set — Mathlib

English

If J is FinallySmall, there exists a small set s and, for every i in J, a nonempty morphism i ⟶ j for some j in s.

Русский

Если J является FinallySmall, существует малое множество s и для каждого i в J непустой морфизм i ⟶ j для некоторого j в s.

LaTeX

$$$\\exists s,\\; \\text{Small}(s)\\; \\land\\; \\forall i,\\; \\exists j\\in s,\\; \\operatorname{Nonempty}(i \\to j)$$$

Lean4

/-- The converse is true if `J` is filtered, see `finallySmall_of_small_weakly_terminal_set`. -/
theorem exists_small_weakly_terminal_set [FinallySmall.{w} J] :
    ∃ (s : Set J) (_ : Small.{w} s), ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
  by
  refine ⟨Set.range (fromFinalModel J).obj, inferInstance, fun i => ?_⟩
  obtain ⟨f⟩ : Nonempty (StructuredArrow i (fromFinalModel J)) := IsConnected.is_nonempty
  exact ⟨(fromFinalModel J).obj f.right, Set.mem_range_self _, ⟨f.hom⟩⟩

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