initiallySmall_iff_exists_small_weakly_initial_set

English

For IsCofilteredOrEmpty J, InitiallySmall J iff there exists a small set with the weakly initial property.

Русский

Для IsCofilteredOrEmpty J, InitiallySmall J эквивалентно существованию малого множества со слабой начальностью.

LaTeX

$$IsCofilteredOrEmpty J ⟺ ∃ s, Small s ∧ ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i)$$

Lean4

theorem initiallySmall_iff_exists_small_weakly_initial_set [IsCofilteredOrEmpty J] :
    InitiallySmall.{v} J ↔ ∃ (s : Set J) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i) :=
  by
  refine ⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩
  rcases h with ⟨s, hs, hs'⟩
  exact initiallySmall_of_small_weakly_initial_set s hs'

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