isCardinalFiltered_preorder — Mathlib

English

If a preorder J and a regular κ with a condition h on boundedness of maps imply the existence of bounds, then IsCardinalFiltered J κ holds.

Русский

Если для предorder J и регулярного κ выполняется условие, что любые отображения имеют ограничение, то IsCardinalFiltered J κ верно.

LaTeX

$$$IsCardinalFiltered\ J\ \kappa$$$

Lean4

theorem isCardinalFiltered_preorder (J : Type w) [Preorder J] (κ : Cardinal.{w}) [Fact κ.IsRegular]
    (h : ∀ ⦃K : Type w⦄ (s : K → J) (_ : Cardinal.mk K < κ), ∃ (j : J), ∀ (k : K), s k ≤ j) : IsCardinalFiltered J κ
    where
  nonempty_cocone
    {A _ F
      hA} :=
    by
    obtain ⟨j, hj⟩ :=
      h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using hasCardinalLT_of_hasCardinalLT_arrow hA)
    exact
      ⟨Cocone.mk j
          { app a := homOfLE (hj a)
            naturality _ _ _ := rfl }⟩

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