CategoryTheory.wellPowered_congr

theorem CategoryTheory.wellPowered_congr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} D], (C ≌ D) → (CategoryTheory.WellPowered C ↔ CategoryTheory.WellPowered D)

The theorem `CategoryTheory.wellPowered_congr` states that the property of a category being well-powered is preserved under equivalences, as long as the two categories involved have their morphisms in the same universe. It takes as input two categories `C` and `D` with their morphisms in the same universe `v`, and an equivalence between `C` and `D`. The theorem then states that if `C` is well-powered then `D` is also well-powered, and vice versa. In category theory, a category is well-powered if every object has a small set of subobjects.

More concisely: If two well-powered categories have their morphisms in the same universe and are equivalent, then each is well-powered if and only if the other is.