instIsCardinalFilteredToTypeOrd — Mathlib

English

The ordinal-to-type cardinal κ.ord.toType κ is card-filtered.

Русский

Кардинал κ.ord.toType κ является кардинал-фильтрованным.

LaTeX

$$$IsCardinalFiltered(\kappa.ord.toType)\kappa$$$

Lean4

instance (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] : IsCardinalFiltered κ.ord.toType κ :=
  isCardinalFiltered_preorder _ _
    (fun ι f hs ↦
      by
      have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
      obtain ⟨j, hj⟩ :=
        Ordinal.lt_cof_type (α := κ.ord.toType) (r := (· < ·)) (S := Set.range f)
          (lt_of_le_of_lt (Cardinal.mk_le_of_surjective h) (lt_of_lt_of_le hs (by simp [hκ.out.cof_eq])))
      exact ⟨j, fun i ↦ (hj (f i) (by simp)).le⟩)

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