BourbakiLean2.Set.FiniteCardinal

source

class Cardinal.Finite (a : Cardinal) :

Prop

neq_plus_one : a ≠ a + 1

Instances

source

@[simp]

theorem Cardinal.Finite.lt_plus_one {a : Cardinal} [h : a.Finite] :

a < a + 1

source

theorem Cardinal.Finite.infer {a : Cardinal} [h : a.Finite] :

a.Finite

source

theorem Cardinal.finite_iff {a : Cardinal} :

a.Finite ↔ a ≠ a + 1

source

def FiniteCardinal :

Type (u + 1)

Equations

FiniteCardinal = { a : Cardinal // a.Finite }

Instances For

source

instance instCoeFiniteCardinalCardinal :

Coe FiniteCardinal Cardinal

Equations

instCoeFiniteCardinalCardinal = { coe := fun (x : FiniteCardinal) => x.val }

source

noncomputable instance instWellOrderFiniteCardinal :

WellOrder FiniteCardinal

Equations

instWellOrderFiniteCardinal = id inferInstance

source

class Finite (α : Type u) :

Prop

finite : (Cardinal.mk α).Finite

Instances

source

instance instFiniteValCardinal {a : FiniteCardinal} :

a.val.Finite

Equations

⋯ = ⋯

source

instance instFiniteMkOfFinite {α : Type u} [Finite α] :

(Cardinal.mk α).Finite

Equations

⋯ = ⋯

source

theorem Finite.iff {α : Type u} :

Finite α ↔ (Cardinal.mk α).Finite

source

def FiniteType :

Type (u + 1)

Equations

FiniteType = { α : Type ?u.1 // Finite α }

Instances For

source

def FiniteType.cardinality' :

FiniteType → FiniteCardinal

Equations

FiniteType.cardinality' ⟨x_1, h⟩ = ⟨Cardinal.mk x_1, ⋯⟩

Instances For

source

theorem Cardinal.finite_iff_add_one_finite {a : Cardinal} :

(a + 1).Finite ↔ a.Finite

source

instance Cardinal.Finite.succ {a : Cardinal} [h : a.Finite] :

(a + 1).Finite

Equations

⋯ = ⋯

source

instance Cardinal.Finite.zero :

Cardinal.Finite 0

Equations

Cardinal.Finite.zero = ⋯

source

instance Cardinal.Finite.one :

Cardinal.Finite 1

Equations

Cardinal.Finite.one = ⋯

source

def Cardinal.ofNat :

Nat → Cardinal

Equations

Cardinal.ofNat 0 = 0
Cardinal.ofNat n.succ = Cardinal.ofNat n + 1

Instances For

source

@[simp]

theorem Cardinal.ofNat_zero :

Cardinal.ofNat 0 = 0

source

@[simp]

theorem Cardinal.ofNat_one :

Cardinal.ofNat 1 = 1

source

theorem Cardinal.Finite.of_le_finite {a b : Cardinal} (h' : b.Finite) (h : a ≤ b) :

a.Finite

source

theorem Cardinal.Finite.has_pred {a : Cardinal} (h : a.Finite) (h' : a ≠ 0) :

∃ (b : Cardinal), a = b + 1

source

theorem Cardinal.Finite.has_unique_pred {a : Cardinal} (h : a.Finite) (h' : a ≠ 0) :

∃! b : Cardinal, a = b + 1

source

noncomputable def Cardinal.Finite.pred {a : Cardinal} (h : a.Finite) (h' : a ≠ 0) :

Cardinal

Equations

h.pred h' = Classical.choose ⋯

Instances For

source

@[simp]

theorem Cardinal.Finite.pred_of_plus_one {a : Cardinal} (h' : (a + 1).Finite) (h'' : a + 1 ≠ 0) :

h'.pred h'' = a

source

@[simp]

theorem Cardinal.Finite.pred_plus_one {a : Cardinal} (h' : a.Finite) (h'' : a ≠ 0) :

h'.pred h'' + 1 = a

source

instance Cardinal.Finite.pred_finite {a : Cardinal} [h : a.Finite] (h' : a ≠ 0) :

(h.pred h').Finite

Equations

⋯ = ⋯

source

theorem Cardinal.Finite.exists_add_iff_lt {a b : Cardinal} (hfin : b.Finite) :

(∃ (c : Cardinal), b = a + c + 1) ↔ a < b

source

theorem Cardinal.Finite.le_pred_iff {a b : Cardinal} (h : a.Finite) (h' : a ≠ 0) :

b < a ↔ b ≤ h.pred h'

source

theorem Cardinal.Finite.lt_add_one_iff {a b : Cardinal} (h : a.Finite) :

b < a + 1 ↔ b ≤ a

source

theorem Finite.of_inj_finite {α β : Type u} [h : Finite β] (f : Function.Injection α β) :

Finite α

bit of finite set stuff

source

theorem Finite.of_surj_finite {α β : Type u} [h : Finite α] (f : Function.Surjection α β) :

Finite β

source

theorem Finite.of_bij_finite {α β : Type u} [h : Finite α] (f : Function.Bijection α β) :

Finite β

source

instance Finite.set {α : Type u} {s : Set α} [h : Finite α] :

Finite ↥s

Equations

⋯ = ⋯

source

instance Finite.subtype {α : Type u} {p : α → Prop} [h : Finite α] :

Finite { x : α // p x }

Equations

⋯ = ⋯

source

theorem Finite.subset {α : Type u} {s t : Set α} [h : Finite ↥s] (h' : t ⊆ s) :

Finite ↥t

source

instance Finite.inter_left {α : Type u} {s t : Set α} [h : Finite ↥s] :

Finite ↥(s ∩ t)

Equations

⋯ = ⋯

source

instance Finite.inter_right {α : Type u} {s t : Set α} [h : Finite ↥t] :

Finite ↥(s ∩ t)

Equations

⋯ = ⋯

source

instance Finite.sdiff {α : Type u} {s t : Set α} [h : Finite ↥s] :

Finite ↥(s \ t)

Equations

⋯ = ⋯

source

instance Finite.iInter_all {α ι : Type u} [ne : Nonempty ι] {x : ι → Set α} [h : ∀ (i : ι), Finite ↥(x i)] :

Finite ↥(⋂ i : ι, x i)

Equations

⋯ = ⋯

source

theorem Finite.iInter_one {α ι : Type u} {x : ι → Set α} {i : ι} [h : Finite ↥(x i)] :

Finite ↥(⋂ i : ι, x i)

source

instance Finite.empty_set {α : Type u} :

Finite ↥∅

Equations

⋯ = ⋯

source

theorem Cardinal.mk_singleton {α : Type u} {a : α} :

Cardinal.mk ↥{a} = 1

source

instance Finite.singleton {α : Type u} {a : α} :

Finite ↥{a}

Equations

⋯ = ⋯

source

theorem Finite.ssubset_cardinal_lt {α : Type u} {s : Set α} [h : Finite α] (h' : s ≠ Set.univ) :

Cardinal.mk ↥s < Cardinal.mk α

source

instance Finite.image {α β : Type u} {s : Set α} [h : Finite ↥s] (f : α → β) :

Finite ↥(f '' s)

Equations

⋯ = ⋯

source

instance Finite.preimage_bij {α β : Type u} {s : Set β} [h : Finite ↥s] (f : Function.Bijection α β) :

Finite ↥(f.val ⁻¹' s)

Equations

⋯ = ⋯

source

theorem Finite.surj_of_inj {α β : Type u} [Finite β] {f : α → β} (hab : Equipotent α β) (h : Function.Injective f) :

Function.Surjective f

source

theorem Finite.inj_of_surj {α β : Type u} [Finite α] {f : α → β} (hab : Equipotent α β) (h : Function.Surjective f) :

Function.Injective f

source

theorem Finite.bij_iff_inj {α β : Type u} [Finite β] {f : α → β} (hab : Equipotent α β) :

Function.Bijective f ↔ Function.Injective f

source

theorem Finite.bij_iff_surj {α β : Type u} [Finite α] {f : α → β} (hab : Equipotent α β) :

Function.Bijective f ↔ Function.Surjective f

source

theorem Cardinal.Finite.induction {p : FiniteCardinal → Prop} (h0 : p ⟨0, Cardinal.Finite.zero⟩) (hs : ∀ (a : FiniteCardinal), p a → p ⟨a.val + 1, ⋯⟩) (a : FiniteCardinal) :

p a

source

theorem Cardinal.Finite.recursion_ex {p : FiniteCardinal → Type u_1} (h0 : p ⟨0, Cardinal.Finite.zero⟩) (hs : (a : FiniteCardinal) → p a → p ⟨a.val + 1, ⋯⟩) :

∃ (f : (x : FiniteCardinal) → p x), f ⟨0, Cardinal.Finite.zero⟩ = h0 ∧ ∀ (a : FiniteCardinal), f ⟨a.val + 1, ⋯⟩ = hs a (f a)

source

noncomputable def FiniteCardinal.recursion {p : FiniteCardinal → Type u_1} (h0 : p ⟨0, Cardinal.Finite.zero⟩) (hs : (a : FiniteCardinal) → p a → p ⟨a.val + 1, ⋯⟩) (a : FiniteCardinal) :

p a

Equations

FiniteCardinal.recursion h0 hs a = ⋯.choose a

Instances For

source

@[simp]

theorem FiniteCardinal.recursion_zero {p : FiniteCardinal → Type u_1} (h0 : p ⟨0, Cardinal.Finite.zero⟩) (hs : (a : FiniteCardinal) → p a → p ⟨a.val + 1, ⋯⟩) :

FiniteCardinal.recursion h0 hs ⟨0, Cardinal.Finite.zero⟩ = h0

source

@[simp]

theorem FiniteCardinal.recursion_succ {p : FiniteCardinal → Type u_1} {x : FiniteCardinal} (h0 : p ⟨0, Cardinal.Finite.zero⟩) (hs : (a : FiniteCardinal) → p a → p ⟨a.val + 1, ⋯⟩) :

FiniteCardinal.recursion h0 hs ⟨x.val + 1, ⋯⟩ = hs x (FiniteCardinal.recursion h0 hs x)

correspondence to normal nats

source

noncomputable def FiniteCardinal.to_nat :

FiniteCardinal → Nat

Equations

FiniteCardinal.to_nat = FiniteCardinal.recursion Nat.zero fun (x : FiniteCardinal) (f : Nat) => f.succ

Instances For

source

noncomputable def FiniteCardinal.of_nat :

Nat → FiniteCardinal

Equations

FiniteCardinal.of_nat 0 = ⟨0, Cardinal.Finite.zero⟩
FiniteCardinal.of_nat n.succ = ⟨(FiniteCardinal.of_nat n).val + 1, ⋯⟩

Instances For

source

@[simp]

theorem FiniteCardinal.to_nat_of_nat {n : Nat} :

(FiniteCardinal.of_nat n).to_nat = n

source

@[simp]

theorem FiniteCardinal.of_nat_to_nat {x : FiniteCardinal} :

FiniteCardinal.of_nat x.to_nat = x

source

@[simp]

theorem FiniteCardinal.of_nat_bij :

Function.Bijective FiniteCardinal.of_nat

source

@[simp]

theorem FiniteCardinal.to_nat_bij :

Function.Bijective FiniteCardinal.to_nat

source

@[simp]

theorem FiniteCardinal.of_nat_zero :

FiniteCardinal.of_nat 0 = ⟨0, ⋯⟩

source

@[simp]

theorem FiniteCardinal.of_nat_one :

FiniteCardinal.of_nat 1 = ⟨1, ⋯⟩

source

@[simp]

theorem FiniteCardinal.to_nat_zero :

FiniteCardinal.to_nat ⟨0, ⋯⟩ = 0

source

@[simp]

theorem FiniteCardinal.to_nat_one :

FiniteCardinal.to_nat ⟨1, ⋯⟩ = 1

source

@[simp]

theorem FiniteCardinal.of_nat_add {n m : Nat} :

(FiniteCardinal.of_nat (n + m)).val = (FiniteCardinal.of_nat n).val + (FiniteCardinal.of_nat m).val

source

@[simp]

theorem FiniteCardinal.of_nat_mul {n m : Nat} :

(FiniteCardinal.of_nat (n * m)).val = (FiniteCardinal.of_nat n).val * (FiniteCardinal.of_nat m).val

source

@[simp]

theorem FiniteCardinal.of_nat_pow {n m : Nat} :

(FiniteCardinal.of_nat (n ^ m)).val = (FiniteCardinal.of_nat n).val ^ (FiniteCardinal.of_nat m).val

source

@[simp]

theorem FiniteCardinal.of_nat_isOrderIso :

IsOrderIso FiniteCardinal.of_nat

source

@[simp]

theorem FiniteCardinal.to_nat_isOrderIso :

IsOrderIso FiniteCardinal.to_nat

source

@[simp]

theorem FiniteCardinal.to_nat_le_iff {x y : FiniteCardinal} :

x.to_nat ≤ y.to_nat ↔ x ≤ y

source

@[simp]

theorem FiniteCardinal.to_nat_lt_iff {x y : FiniteCardinal} :

x.to_nat < y.to_nat ↔ x < y

source

@[simp]

theorem FiniteCardinal.of_nat_le_iff {n m : Nat} :

FiniteCardinal.of_nat n ≤ FiniteCardinal.of_nat m ↔ n ≤ m

source

@[simp]

theorem FiniteCardinal.of_nat_lt_iff {n m : Nat} :

FiniteCardinal.of_nat n < FiniteCardinal.of_nat m ↔ n < m

source

instance instFiniteEmpty :

Finite Empty

Equations

instFiniteEmpty = ⋯

source

instance instFinitePEmpty :

Finite PEmpty

Equations

instFinitePEmpty = ⋯

source

instance instFinitePUnit :

Finite PUnit

Equations

instFinitePUnit = ⋯

source

instance instFiniteUnit :

Finite Unit

Equations

instFiniteUnit = ⋯

source

instance instFiniteBool :

Finite Bool

Equations

instFiniteBool = ⋯

source

instance instFiniteSum {α β : Type u} [Finite α] [Finite β] :

Finite (α ⊕ β)

Equations

⋯ = ⋯

source

instance instFiniteProd {α β : Type u} [Finite α] [Finite β] :

Finite (α × β)

Equations

⋯ = ⋯

source

instance instFiniteForall {α β : Type u} [Finite α] [Finite β] :

Finite (α → β)

Equations

⋯ = ⋯

source

instance instFiniteInjection {α β : Type u} [Finite α] [Finite β] :

Finite (Function.Injection α β)

Equations

⋯ = ⋯

source

instance instFiniteSurjection {α β : Type u} [Finite α] [Finite β] :

Finite (Function.Surjection α β)

Equations

⋯ = ⋯

source

instance instFiniteBijection {α β : Type u} [Finite α] [Finite β] :

Finite (Function.Bijection α β)

Equations

⋯ = ⋯

source

instance instFiniteOfSubsingleton {α : Type u} [Subsingleton α] :

Finite α

Equations

⋯ = ⋯

source

instance sum_finite {a b : Cardinal} [ha : a.Finite] [hb : b.Finite] :

(a + b).Finite

Equations

⋯ = ⋯

source

instance mul_finite {a b : Cardinal} [ha : a.Finite] [hb : b.Finite] :

(a * b).Finite

Equations

⋯ = ⋯

source

instance pow_finite {a b : Cardinal} [ha : a.Finite] [hb : b.Finite] :

(a ^ b).Finite

Equations

⋯ = ⋯

source

@[simp]

theorem FiniteCardinal.to_nat_add {x y : FiniteCardinal} :

FiniteCardinal.to_nat ⟨x.val + y.val, ⋯⟩ = x.to_nat + y.to_nat

source

@[simp]

theorem FiniteCardinal.to_nat_mul {x y : FiniteCardinal} :

FiniteCardinal.to_nat ⟨x.val * y.val, ⋯⟩ = x.to_nat * y.to_nat

source

@[simp]

theorem FiniteCardinal.to_nat_pow {x y : FiniteCardinal} :

FiniteCardinal.to_nat ⟨x.val ^ y.val, ⋯⟩ = x.to_nat ^ y.to_nat

source

instance instFiniteSubtypeMemSetUnion {α : Type u} {a b : Set α} [Finite ↥a] [Finite ↥b] :

Finite ↥(a ∪ b)

Equations

⋯ = ⋯

source

instance instFiniteSubtypeMemSetInsert {α : Type u} {a : Set α} {b : α} [Finite ↥a] :

Finite ↥(insert b a)

Equations

⋯ = ⋯

source

theorem FiniteCardinal.equipotent_of_nat_eq {n : Nat} {α : Type u} {β : Type v} [Finite α] [Finite β] (h1 : Cardinal.mk α = (FiniteCardinal.of_nat n).val) (h2 : Cardinal.mk β = (FiniteCardinal.of_nat n).val) :

Equipotent α β

source

instance Finite.sets {α : Type u} [h : Finite α] :

Finite (Set α)

Equations

⋯ = ⋯