isPresentable — Mathlib

English

If h is a κ-filtered generators structure for a family G, then each generator G_i is presentable.

Русский

Если существует структура κ-фильтрованных генераторов для семейства G, то каждый генератор G_i презентабельный.

LaTeX

$$$\forall i, IsPresentable(G_i)$$$

Lean4

theorem isPresentable (i : ι) : IsPresentable.{w} (G i) :=
  have := h.isCardinalPresentable
  isPresentable_of_isCardinalPresentable _ κ

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