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 κ