isFiltered_of_isCardinalFiltered — Mathlib

English

For a category J, IsCardinalFiltered J aleph0 iff IsFiltered J.

Русский

Для категории J условие IsCardinalFiltered J aleph0 эквивалентно IsFiltered J.

LaTeX

$$$IsCardinalFiltered(J, \aleph_0) \iff IsFiltered(J)$$$

Lean4

theorem isFiltered_of_isCardinalFiltered (J : Type u) [Category.{v} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
    [IsCardinalFiltered J κ] : IsFiltered J :=
  by
  rw [IsFiltered.iff_cocone_nonempty.{w}]
  intro A _ _ F
  have hA : HasCardinalLT (Arrow A) κ :=
    by
    refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
    simp only [hasCardinalLT_aleph0_iff]
    infer_instance
  exact ⟨cocone F hA⟩

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