noncomputable def Finite.ftype (x : Type u_5) [h : Finite x] : FiniteType

Equations

• Finite.ftype x = ⟨x, h⟩

@[simp]

theorem Finite.ftype_finiteType_val (x : FiniteType) : Finite.ftype x.val = x

noncomputable def FiniteType.cardinality (x : FiniteType) : Nat

Equations

• x.cardinality = x.cardinality'.to_nat

@[simp]

theorem FiniteType.cardinality_empty : (Finite.ftype Empty).cardinality = 0

@[simp]

theorem FiniteType.cardinality_empty_set {α : Type u_1} : (Finite.ftype ↥∅).cardinality = 0

@[simp]

theorem FiniteType.cardinality_pempty : (Finite.ftype PEmpty).cardinality = 0

@[simp]

theorem FiniteType.cardinality_unit : (Finite.ftype Unit).cardinality = 1

@[simp]

theorem FiniteType.cardinality_unique {α : Type u_1} [Unique α] : (Finite.ftype α).cardinality = 1

@[simp]

theorem FiniteType.cardinality_punit : (Finite.ftype PUnit).cardinality = 1

@[simp]

theorem FiniteType.cardinality_sum {α β : Type u} [Finite α] [Finite β] : (Finite.ftype (α ⊕ β)).cardinality = (Finite.ftype α).cardinality + (Finite.ftype β).cardinality

@[simp]

theorem FiniteType.cardinality_mul {α β : Type u} [Finite α] [Finite β] : (Finite.ftype (α × β)).cardinality = (Finite.ftype α).cardinality * (Finite.ftype β).cardinality

@[simp]

theorem FiniteType.cardinality_pow {α β : Type u} [Finite α] [Finite β] : (Finite.ftype (α → β)).cardinality = (Finite.ftype β).cardinality ^ (Finite.ftype α).cardinality

@[simp]

theorem FiniteType.cardinality_le_iff {a b : FiniteType} : a.cardinality ≤ b.cardinality ↔ Nonempty (Function.Injection a.val b.val)

@[simp]

theorem FiniteType.cardinality_le_ftype_iff {α β : Type u} [Finite α] [Finite β] : (Finite.ftype α).cardinality ≤ (Finite.ftype β).cardinality ↔ Nonempty (Function.Injection α β)

theorem FiniteType.cardinality_univ {α : Type u} [Finite α] : (Finite.ftype ↥Set.univ).cardinality = (Finite.ftype α).cardinality

theorem FiniteType.cardinality_le_of_surj {a b : FiniteType} (h : Function.Surjection a.val b.val) : b.cardinality ≤ a.cardinality

theorem FiniteType.cardinality_le_ftype_of_surj {α β : Type u} [Finite α] [Finite β] (h : Function.Surjection β α) : (Finite.ftype α).cardinality ≤ (Finite.ftype β).cardinality

@[simp]

theorem FiniteType.cardinality_eq_iff {a b : FiniteType} : a.cardinality = b.cardinality ↔ Equipotent a.val b.val

@[simp]

theorem FiniteType.cardinality_eq_iff' {α β : Type u} [Finite α] [Finite β] : (Finite.ftype α).cardinality = (Finite.ftype β).cardinality ↔ Equipotent α β

theorem FiniteType.cardinality_le_of_subset {α : Type u} {a b : Set α} (h : a ⊆ b) [h' : Finite ↥a] [h'' : Finite ↥b] : (Finite.ftype ↥a).cardinality ≤ (Finite.ftype ↥b).cardinality

theorem FiniteType.cardinality_image_le {α β : Type u} {a : Set α} {f : α → β} [h' : Finite ↥a] : (Finite.ftype ↥(f '' a)).cardinality ≤ (Finite.ftype ↥a).cardinality

theorem FiniteType.cardinality_image_eq_inj {α β : Type u} {a : Set α} {f : α → β} [h' : Finite ↥a] (h'' : Function.Injective f) : (Finite.ftype ↥(f '' a)).cardinality = (Finite.ftype ↥a).cardinality

theorem FiniteType.cardinality_preimage_eq_bij {α β : Type u} {a : Set β} (f : Function.Bijection α β) [h' : Finite ↥a] : (Finite.ftype ↥(f.val ⁻¹' a)).cardinality = (Finite.ftype ↥a).cardinality

@[simp]

theorem FiniteType.cardinality_set_le {α : Type u} {a : Set α} [Finite α] : (Finite.ftype ↥a).cardinality ≤ (Finite.ftype α).cardinality

@[simp]

theorem FiniteType.cardinality_set_zero_iff {α : Type u} {a : Set α} [Finite ↥a] : (Finite.ftype ↥a).cardinality = 0 ↔ a = ∅

theorem FiniteType.of_cardinality_zero {α : Type u} [Finite α] (h : (Finite.ftype α).cardinality = 0) (h2 : α) : False

@[simp]

theorem FiniteType.cardinality_singleton {α : Type u} {x : α} : (Finite.ftype ↥{x}).cardinality = 1

@[simp]

theorem FiniteType.cardinality_manual_insert {α : Type u} {a : Set α} [Finite ↥a] {x : α} (h' : ¬x ∈ a) : (Finite.ftype ↥({x} ∪ a)).cardinality = (Finite.ftype ↥a).cardinality + 1

theorem FiniteType.cardinality_preimage_same_product {α β : Type u} [Finite α] [Finite β] {f : α → β} {n : Nat} (h' : ∀ (y : β), (Finite.ftype ↥(f ⁻¹' {y})).cardinality = n) : (Finite.ftype α).cardinality = n * (Finite.ftype β).cardinality

@[simp]

theorem FiniteType.cardinality_insert {α : Type u} {a : Set α} [Finite ↥a] {x : α} (h' : ¬x ∈ a) : (Finite.ftype ↥(insert x a)).cardinality = (Finite.ftype ↥a).cardinality + 1

theorem FiniteType.eq_of_cardinality_eq_subset {α : Type u} {a b : Set α} [Finite ↥a] [Finite ↥b] (h : a ⊆ b) (h' : (Finite.ftype ↥a).cardinality = (Finite.ftype ↥b).cardinality) : a = b

theorem FiniteType.cardinality_disj_union {α : Type u} [Finite α] {a b : Set α} (h : a ∩ b = ∅) : (Finite.ftype ↥(a ∪ b)).cardinality = (Finite.ftype ↥a).cardinality + (Finite.ftype ↥b).cardinality

@[simp]

theorem FiniteType.cardinality_compl {α : Type u} [Finite α] {a : Set α} : (Finite.ftype ↥aᶜ).cardinality = (Finite.ftype α).cardinality - (Finite.ftype ↥a).cardinality

theorem FiniteType.cardinality_nonempty {α : Type u} [Finite α] [h : Nonempty α] : 1 ≤ (Finite.ftype α).cardinality

theorem FiniteType.nonempty_of_cardinality_succ {α : Type u} {n : Nat} [Finite α] (h : (Finite.ftype α).cardinality = n + 1) : Nonempty α

theorem FiniteType.cardinality_sets {α : Type u} [Finite α] : (Finite.ftype (Set α)).cardinality = 2 ^ (Finite.ftype α).cardinality

@[simp]

theorem FiniteType.cardinality_diag {α : Type u} [Finite α] : (Finite.ftype ↥Relation.diag).cardinality = (Finite.ftype α).cardinality

theorem Finite.set_induction {α : Type u_5} {p : Set α → Prop} (he : p ∅) (hs : ∀ (x : α) (a : Set α), Finite ↥a → ¬x ∈ a → p a → p (a ∪ {x})) (a : Set α) [_h : Finite ↥a] : p a