wellPowered_of_equiv — Mathlib

English

If e: C ≌ D is an equivalence of categories, then C is WellPowered iff D is WellPowered; equivalently, well-powered is preserved by categorical equivalences.

Русский

Если e: C ≌ D — эквивалентность категорий, то C is WellPowered тогда и только тогда, когда D — WellPowered; устойчивость к эквивалентностям.

LaTeX

$$$\forall C,D\, (e:C\simeq D),\ \mathrm{WellPowered}(C) \iff \mathrm{WellPowered}(D).$$$

Lean4

theorem wellPowered_of_equiv (e : C ≌ D) [LocallySmall.{w} C] [LocallySmall.{w} D] [WellPowered.{w} C] :
    WellPowered.{w} D :=
  wellPowered_of_essentiallySmall_monoOver fun X =>
    (essentiallySmall_congr (MonoOver.congr X e.symm)).2 <| by infer_instance

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