Properties of objects that are bounded by a cardinal #
Given P : ObjectProperty C and κ : Cardinal, we introduce a predicate
P.HasCardinalLT κ saying that the cardinality of Subtype P is < κ.
@[reducible, inline]
abbrev CategoryTheory.ObjectProperty.HasCardinalLT {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) :
The property that the subtype of objects satisfying a property P : ObjectProperty C
is of cardinality < κ.
Equations
- P.HasCardinalLT κ = HasCardinalLT (Subtype P) κ
Instances For
theorem CategoryTheory.ObjectProperty.hasCardinalLT_subtype_ofObj {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ι → C) {κ : Cardinal.{w}} (h : HasCardinalLT ι κ) :
(ofObj X).HasCardinalLT κ
theorem CategoryTheory.ObjectProperty.HasCardinalLT.iSup {C : Type u} [Category.{v, u} C] {ι : Type u_1} {P : ι → ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (hP : ∀ (i : ι), (P i).HasCardinalLT κ) (hι : HasCardinalLT ι κ) :
(⨆ (i : ι), P i).HasCardinalLT κ
theorem CategoryTheory.ObjectProperty.HasCardinalLT.sup {C : Type u} [Category.{v, u} C] {P₁ P₂ : ObjectProperty C} {κ : Cardinal.{w}} (h₁ : P₁.HasCardinalLT κ) (h₂ : P₂.HasCardinalLT κ) (hκ : Cardinal.aleph0 ≤ κ) :
(P₁ ⊔ P₂).HasCardinalLT κ