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