Documentation

Mathlib.SetTheory.Cardinal.HasCardinalLT

The property of being of cardinality less than a cardinal #

Given X : Type u and κ : Cardinal.{v}, we introduce a predicate HasCardinalLT X κ expressing that Cardinal.lift.{v} (Cardinal.mk X) < Cardinal.lift κ.

source
def HasCardinalLT (X : Type u) (κ : Cardinal.{v}) :
Prop

The property that the cardinal of a type X : Type u is less than κ : Cardinal.{v}.

Equations
Instances For
    source
    theorem hasCardinalLT_iff_cardinal_mk_lt (X : Type u) (κ : Cardinal.{u}) :
    HasCardinalLT X κ ↔ Cardinal.mk X < κ
    source
    theorem HasCardinalLT.small {X : Type u} {κ : Cardinal.{v}} (h : HasCardinalLT X κ) :
    Small.{v, u} X
    source
    theorem HasCardinalLT.of_le {X : Type u} {κ : Cardinal.{v}} (h : HasCardinalLT X κ) {κ' : Cardinal.{v}} (hκ' : κ ≤ κ') :
    HasCardinalLT X κ'
    source
    theorem HasCardinalLT.of_injective {X : Type u} {κ : Cardinal.{v}} (h : HasCardinalLT X κ) {Y : Type u'} (f : Y → X) (hf : Function.Injective f) :
    HasCardinalLT Y κ
    source
    theorem HasCardinalLT.of_surjective {X : Type u} {κ : Cardinal.{v}} (h : HasCardinalLT X κ) {Y : Type u'} (f : X → Y) (hf : Function.Surjective f) :
    HasCardinalLT Y κ
    source
    theorem hasCardinalLT_iff_of_equiv {X : Type u} {Y : Type u'} (e : X ≃ Y) (κ : Cardinal.{v}) :
    HasCardinalLT X κ ↔ HasCardinalLT Y κ
    source
    @[simp]
    theorem hasCardinalLT_aleph0_iff (X : Type u) :
    HasCardinalLT X Cardinal.aleph0 ↔ Finite X
    source
    theorem hasCardinalLT_sum_iff (X : Type u) (Y : Type u') (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ
    source
    theorem hasCardinalLT_option_iff (X : Type u) (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ
    source
    theorem HasCardinalLT.exists_regular_cardinal (X : Type u) [Small.{w, u} X] :
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ HasCardinalLT X κ

    For any w-small type X, there exists a regular cardinal κ : Cardinal.{w} such that HasCardinalLT X κ.

    source
    theorem HasCardinalLT.exists_regular_cardinal_forall {ι : Type v} {X : ι → Type u} [Small.{w, v} ι] [∀ (i : ι), Small.{w, u} (X i)] :
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

    For any w-small family X : ι → Type u of w-small types, there exists a regular cardinal κ : Cardinal.{w} such that HasCardinalLT (X i) κ for all i : ι.