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_of_finite (X : Type u_1) [Finite X] (κ : Cardinal.{u_2}) (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT X κ
    source
    @[simp]
    theorem hasCardinalLT_lift_iff (X : Type v) (κ : Cardinal.{w}) :
    HasCardinalLT X (Cardinal.lift.{u, w} κ) ↔ HasCardinalLT X κ
    source
    @[simp]
    theorem hasCardinalLT_ulift_iff (X : Type v) (κ : Cardinal.{w}) :
    HasCardinalLT (ULift.{u, v} X) κ ↔ HasCardinalLT 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_subtype_max {X : Type u_1} {P₁ P₂ : X → Prop} {κ : Cardinal.{u_2}} (hκ : Cardinal.aleph0 ≤ κ) (h₁ : HasCardinalLT (Subtype P₁) κ) (h₂ : HasCardinalLT (Subtype P₂) κ) :
    HasCardinalLT (Subtype (P₁ ⊔ P₂)) κ
    source
    theorem hasCardinalLT_union {X : Type u_1} {S₁ S₂ : Set X} {κ : Cardinal.{u_2}} (hκ : Cardinal.aleph0 ≤ κ) (h₁ : HasCardinalLT (↑S₁) κ) (h₂ : HasCardinalLT (↑S₂) κ) :
    HasCardinalLT (↑(S₁ ∪ S₂)) κ
    source
    theorem hasCardinalLT_sigma' {ι : Type w} (α : ι → Type w) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hι : HasCardinalLT ι κ) (hα : ∀ (i : ι), HasCardinalLT (α i) κ) :
    HasCardinalLT ((i : ι) × α i) κ

    The particular case of hasCardinatLT_sigma when all the inputs are in the same universe w. It is used to prove the general case.

    source
    theorem hasCardinalLT_sigma {ι : Type u} (α : ι → Type v) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hι : HasCardinalLT ι κ) (hα : ∀ (i : ι), HasCardinalLT (α i) κ) :
    HasCardinalLT ((i : ι) × α i) κ
    source
    theorem hasCardinalLT_subtype_iSup {ι : Type u_1} {X : Type u_2} (P : ι → X → Prop) {κ : Cardinal.{u_3}} [Fact κ.IsRegular] (hι : HasCardinalLT ι κ) (hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ) :
    HasCardinalLT (Subtype (⨆ (i : ι), P i)) κ
    source
    theorem hasCardinalLT_iUnion {ι : Type u_1} {X : Type u_2} (S : ι → Set X) {κ : Cardinal.{u_3}} [Fact κ.IsRegular] (hι : HasCardinalLT ι κ) (hS : ∀ (i : ι), HasCardinalLT (↑(S i)) κ) :
    HasCardinalLT (↑(⋃ (i : ι), S i)) κ
    source
    theorem hasCardinalLT_prod' {T₁ T₂ : Type w} {κ : Cardinal.{w}} (hκ : Cardinal.aleph0 ≤ κ) (h₁ : HasCardinalLT T₁ κ) (h₂ : HasCardinalLT T₂ κ) :
    HasCardinalLT (T₁ × T₂) κ

    The particular case of hasCardinatLT_prod when all the inputs are in the same universe w. It is used to prove the general case.

    source
    theorem hasCardinalLT_prod {T₁ : Type u} {T₂ : Type u'} {κ : Cardinal.{w}} (hκ : Cardinal.aleph0 ≤ κ) (h₁ : HasCardinalLT T₁ κ) (h₂ : HasCardinalLT T₂ κ) :
    HasCardinalLT (T₁ × T₂) κ
    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 : ι.