isCardinalFiltered_aleph0_iff — Mathlib

English

For a preorder J and regular κ, a sufficient condition h implies IsCardinalFiltered J κ.

Русский

Для предвариантной частной упорядоченности J и регулярного κ, условие h даёт IsCardinalFiltered J κ.

LaTeX

$$$IsCardinalFiltered J κ$$$

Lean4

theorem isCardinalFiltered_aleph0_iff (J : Type u) [Category.{v} J] :
    IsCardinalFiltered J Cardinal.aleph0.{w} ↔ IsFiltered J :=
  by
  constructor
  · intro
    exact isFiltered_of_isCardinalFiltered J Cardinal.aleph0
  · intro
    constructor
    intro A _ F hA
    rw [hasCardinalLT_aleph0_iff] at hA
    have := ((Arrow.finite_iff A).1 hA).some
    exact ⟨IsFiltered.cocone F⟩

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