instIsCardinalFilteredJ — Mathlib

English

For any G: ι → C and κ regular, if h = AreCardinalFilteredGenerators G κ, then for each X, (h.J X) is κ-filtered.

Русский

Для любого G: ι → C и κ регулярного, если h = AreCardinalFilteredGenerators G κ, то для каждого X выполнено, что (h.J X) κ-фильтрованно.

LaTeX

$$$\text{IsCardinalFiltered } (h.J X) \kappa$$$

Lean4

noncomputable instance : IsCardinalFiltered (h.J X) κ :=
  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose

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