Documentation

Mathlib.Deprecated.Cardinal.Finite

Deprecated material on PartENat.card. #

source
@[deprecated ENat.card]
def PartENat.card (α : Type u_1) :
PartENat

PartENat.card α is the cardinality of α as an extended natural number. If α is infinite, PartENat.card α = ⊤.

Equations
Instances For
    source
    @[simp]
    theorem PartENat.card_eq_coe_fintype_card {α : Type u} [Fintype α] :
    PartENat.card α = ↑(Fintype.card α)
    source
    @[simp]
    theorem PartENat.card_eq_top_of_infinite {α : Type u} [Infinite α] :
    PartENat.card α = ⊤
    source
    @[simp]
    theorem PartENat.card_sum (α : Type u_1) (β : Type u_2) :
    PartENat.card (α ⊕ β) = PartENat.card α + PartENat.card β
    source
    theorem PartENat.card_congr {α : Type u_1} {β : Type u_2} (f : α ≃ β) :
    PartENat.card α = PartENat.card β
    source
    @[simp]
    theorem PartENat.card_ulift (α : Type u_1) :
    PartENat.card (ULift.{u_2, u_1} α) = PartENat.card α
    source
    @[simp]
    theorem PartENat.card_plift (α : Type u_1) :
    PartENat.card (PLift α) = PartENat.card α
    source
    theorem PartENat.card_image_of_injOn {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h : Set.InjOn f s) :
    PartENat.card ↑(f '' s) = PartENat.card ↑s
    source
    theorem PartENat.card_image_of_injective {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Function.Injective f) :
    PartENat.card ↑(f '' s) = PartENat.card ↑s
    source
    @[simp]
    theorem Cardinal.natCast_le_toPartENat_iff {n : ℕ} {c : Cardinal.{u_1}} :
    ↑n ≤ Cardinal.toPartENat c ↔ ↑n ≤ c
    source
    @[simp]
    theorem Cardinal.toPartENat_le_natCast_iff {c : Cardinal.{u_1}} {n : ℕ} :
    Cardinal.toPartENat c ≤ ↑n ↔ c ≤ ↑n
    source
    @[simp]
    theorem Cardinal.natCast_eq_toPartENat_iff {n : ℕ} {c : Cardinal.{u_1}} :
    ↑n = Cardinal.toPartENat c ↔ ↑n = c
    source
    @[simp]
    theorem Cardinal.toPartENat_eq_natCast_iff {c : Cardinal.{u_1}} {n : ℕ} :
    Cardinal.toPartENat c = ↑n ↔ c = ↑n
    source
    @[simp]
    theorem Cardinal.natCast_lt_toPartENat_iff {n : ℕ} {c : Cardinal.{u_1}} :
    ↑n < Cardinal.toPartENat c ↔ ↑n < c
    source
    @[simp]
    theorem Cardinal.toPartENat_lt_natCast_iff {n : ℕ} {c : Cardinal.{u_1}} :
    Cardinal.toPartENat c < ↑n ↔ c < ↑n
    source
    theorem PartENat.card_eq_zero_iff_empty (α : Type u_1) :
    PartENat.card α = 0 ↔ IsEmpty α
    source
    theorem PartENat.card_le_one_iff_subsingleton (α : Type u_1) :
    PartENat.card α ≤ 1 ↔ Subsingleton α
    source
    theorem PartENat.one_lt_card_iff_nontrivial (α : Type u_1) :
    1 < PartENat.card α ↔ Nontrivial α
    source
    @[deprecated ENat.card_eq_coe_natCard]
    theorem PartENat.card_eq_coe_natCard (α : Type u_1) [Finite α] :
    PartENat.card α = ↑(Nat.card α)
    source
    @[deprecated PartENat.card_eq_coe_natCard]
    theorem PartENat.card_eq_coe_nat_card (α : Type u_1) [Finite α] :
    PartENat.card α = ↑(Nat.card α)

    Alias of PartENat.card_eq_coe_natCard.