BourbakiLean2.Data.Nat.IndexedOps

source

instance finite_sigma {α : Type u} {x : α → Cardinal} [h1 : Finite α] [h2 : ∀ (a : α), (x a).Finite] :

(Cardinal.sigma x).Finite

Equations

⋯ = ⋯

source

instance finite_prod {α : Type u} {x : α → Cardinal} [h1 : Finite α] [h2 : ∀ (a : α), (x a).Finite] :

(Cardinal.prod x).Finite

Equations

⋯ = ⋯

source

instance Finite.prod_finite {α : Type u} [Finite α] {x : α → Type u} [∀ (i : α), Finite (x i)] :

Finite ((i : α) × x i)

Equations

⋯ = ⋯

source

instance Finite.sigma_finite {α : Type u} [Finite α] {x : α → Type u} [∀ (i : α), Finite (x i)] :

Finite ((i : α) → x i)

Equations

⋯ = ⋯

source

instance Finite.pow_finite {α : Type u} [Finite α] :

Finite (Set α)

Equations

⋯ = ⋯

source

instance instFiniteSubtypeMemSetIUnion {α β : Type u} [Finite α] {x : α → Set β} [∀ (i : α), Finite ↥(x i)] :

Finite ↥(⋃ i : α, x i)

Equations

⋯ = ⋯

source

noncomputable def Nat.finite_sum {ι : Type u_1} [Finite ι] (x : ι → Nat) :

Nat

Equations

Nat.finite_sum x = FiniteCardinal.to_nat ⟨Cardinal.sigma fun (i : ι) => (FiniteCardinal.of_nat (x i)).val, ⋯⟩

Instances For

source

noncomputable def Nat.finite_prod {ι : Type u_1} [Finite ι] (x : ι → Nat) :

Nat

Equations

Nat.finite_prod x = FiniteCardinal.to_nat ⟨Cardinal.prod fun (i : ι) => (FiniteCardinal.of_nat (x i)).val, ⋯⟩

Instances For

source

@[simp]

theorem Nat.finite_sum_empty {ι : Type u_1} [Finite ι] (x : ι → Nat) (h : ι → False) :

Nat.finite_sum x = 0

source

@[simp]

theorem Nat.finite_prod_empty {ι : Type u_1} [Finite ι] (x : ι → Nat) (h : ι → False) :

Nat.finite_prod x = 1

source

@[simp]

theorem Nat.finite_sum_unique {ι : Type v} [h : Unique ι] (x : ι → Nat) :

Nat.finite_sum x = x default

source

@[simp]

theorem Nat.finite_prod_unique {ι : Type v} [h : Unique ι] (x : ι → Nat) :

Nat.finite_prod x = x default

source

@[simp]

theorem Nat.finite_sum_reindex {ι ι' : Type v} [h : Finite ι] [h' : Finite ι'] (f : Function.Bijection ι' ι) {x : ι → Nat} :

Nat.finite_sum x = Nat.finite_sum (x ∘ f.val)

source

theorem Nat.finite_sum_reindex_univ {ι : Type v} [h : Finite ι] {x : ι → Nat} :

Nat.finite_sum x = Nat.finite_sum fun (i : ↥Set.univ) => x i.val

source

@[simp]

theorem Nat.finite_prod_reindex {ι ι' : Type v} [h : Finite ι] [h' : Finite ι'] (f : Function.Bijection ι' ι) {x : ι → Nat} :

Nat.finite_prod x = Nat.finite_prod (x ∘ f.val)

source

theorem Nat.finite_prod_reindex_univ {ι : Type v} [h : Finite ι] {x : ι → Nat} :

Nat.finite_prod x = Nat.finite_prod fun (i : ↥Set.univ) => x i.val

source

theorem Nat.finite_sum_assoc {ι ι' : Type v} [h : Finite ι] [h' : Finite ι'] {α : ι → Nat} {p : ι' → Set ι} (h'' : Set.IsPartition p) :

Nat.finite_sum α = Nat.finite_sum fun (i' : ι') => Nat.finite_sum fun (i : ↥(p i')) => α i.val

source

theorem Nat.finite_prod_assoc {ι ι' : Type v} [h : Finite ι] [h' : Finite ι'] {α : ι → Nat} {p : ι' → Set ι} (h'' : Set.IsPartition p) :

Nat.finite_prod α = Nat.finite_prod fun (i' : ι') => Nat.finite_prod fun (i : ↥(p i')) => α i.val

source

theorem Nat.finite_sum_assoc2 {ι : Type u} {α : ι → Nat} [h : Finite ι] {s t : Set ι} (h' : s ∪ t = Set.univ) (h'' : s ∩ t = ∅) :

Nat.finite_sum α = Nat.finite_sum (α ∘ Subtype.val) + Nat.finite_sum (α ∘ Subtype.val)

source

theorem Nat.finite_prod_assoc2 {ι : Type u} {α : ι → Nat} [h : Finite ι] {s t : Set ι} (h' : s ∪ t = Set.univ) (h'' : s ∩ t = ∅) :

Nat.finite_prod α = Nat.finite_prod (α ∘ Subtype.val) * Nat.finite_prod (α ∘ Subtype.val)

source

theorem Nat.finite_sum_remove_one {ι : Type v} [h : Finite ι] {α : ι → Nat} (i : ι) :

Nat.finite_sum α = Nat.finite_sum (α ∘ Subtype.val) + α i

source

theorem Nat.finite_prod_remove_one {ι : Type v} [h : Finite ι] {α : ι → Nat} (i : ι) :

Nat.finite_prod α = Nat.finite_prod (α ∘ Subtype.val) * α i

source

theorem Nat.finite_sum_mono {ι : Type v} [h : Finite ι] {x y : ι → Nat} (h' : ∀ (i : ι), x i ≤ y i) :

Nat.finite_sum x ≤ Nat.finite_sum y

source

theorem Nat.finite_sum_lt {ι : Type v} [h : Finite ι] {x y : ι → Nat} {i : ι} (h' : ∀ (i : ι), x i ≤ y i) (h'' : x i < y i) :

Nat.finite_sum x < Nat.finite_sum y

source

@[simp]

theorem Nat.finite_sum_zero_iff {ι : Type v} [h : Finite ι] {x : ι → Nat} :

Nat.finite_sum x = 0 ↔ ∀ (i : ι), x i = 0

source

@[simp]

theorem Nat.finite_prod_zero_iff {ι : Type v} [h : Finite ι] {x : ι → Nat} :

Nat.finite_prod x = 0 ↔ ∃ (i : ι), x i = 0

source

theorem Nat.finite_prod_mono {ι : Type v} [h : Finite ι] {x y : ι → Nat} (h' : ∀ (i : ι), x i ≤ y i) :

Nat.finite_prod x ≤ Nat.finite_prod y

source

theorem Nat.finite_prod_lt {ι : Type v} [h : Finite ι] {x y : ι → Nat} {i : ι} (h' : ∀ (i : ι), x i ≤ y i) (h'' : x i < y i) (h''' : ∀ (i : ι), 0 < x i) :

Nat.finite_prod x < Nat.finite_prod y

source

theorem Nat.pow_strict_mono_left {a a' b : Nat} (h : 0 < b) (h' : a < a') :

a ^ b < a' ^ b

source

theorem Nat.sub_add_sub {a b a' b' : Nat} (h : a ≤ b) (h' : a' ≤ b') :

b - a + (b' - a') = b + b' - (a + a')

source

theorem Nat.mul_finite_sum {ι : Type v} [Finite ι] {x : ι → Nat} {n : Nat} :

(Nat.finite_sum fun (i : ι) => n * x i) = n * Nat.finite_sum x

source

theorem Nat.finite_prod_pow {ι : Type v} [Finite ι] {x : ι → Nat} {n : Nat} :

(Nat.finite_prod fun (i : ι) => x i ^ n) = Nat.finite_prod x ^ n

source

theorem FiniteType.cardinality_disj_iUnion {α ι : Type u} [Finite α] [Finite ι] {a : ι → Set α} (h : Set.Disjoint a) :

(Finite.ftype ↥(⋃ i : ι, a i)).cardinality = Nat.finite_sum fun (i : ι) => (Finite.ftype ↥(a i)).cardinality