finallySmall_iff_exists_small_weakly_terminal_set

English

For IsFilteredOrEmpty J, FinallySmall J is equivalent to existence of a small set s with a terminal condition.

Русский

Для IsFilteredOrEmpty J FinallySmall J эквивалентно существованию малого множества s с условием терминальности.

LaTeX

$$$[\\text{IsFilteredOrEmpty } J] \\Rightarrow (\\text{FinallySmall } J \\iff \\exists s\\; \\text{Small } s \\land \\exists f: \\text{ ...})$$$

Lean4

theorem finallySmall_iff_exists_small_weakly_terminal_set [IsFilteredOrEmpty J] :
    FinallySmall.{v} J ↔ ∃ (s : Set J) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
  by
  refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩
  rcases h with ⟨s, hs, hs'⟩
  exact finallySmall_of_small_weakly_terminal_set s hs'

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