instWellPoweredShrinkHoms — Mathlib

English

The shrink-homs construction preserves well-poweredness: ShrinkHoms C is WellPowered provided C is LocallySmall and WellPowered.

Русский

Упрощенная конструкция ShrinkHoms сохраняет хорошее свойство: ShrinkHoms C является WellPowered при условии LocallySmall и WellPowered.

LaTeX

$$$\text{WellPowered}(\mathrm{ShrinkHoms}(C))$$$

Lean4

instance [LocallySmall.{w} C] [WellPowered.{w} C] : WellPowered.{w, w} (ShrinkHoms C) :=
  wellPowered_of_equiv.{w} (ShrinkHoms.equivalence.{w} C)

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