mathlib documentation

data.pi

Instances and theorems on pi types #

This file provides basic definitions and notation instances for Pi types.

Instances of more sophisticated classes are defined in pi.lean files elsewhere.

1, 0, +, *, -, ⁻¹, and / are defined pointwise.

source
@[protected, instance]
def pi.has_zero {I : Type u} {f : I → Type v₁} [Π (i : I), has_zero (f i)] :
has_zero (Π (i : I), f i)
source
@[protected, instance]
def pi.has_one {I : Type u} {f : I → Type v₁} [Π (i : I), has_one (f i)] :
has_one (Π (i : I), f i)
Equations
source
@[simp]
theorem pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [Π (i : I), has_zero (f i)] :
0 i = 0
source
@[simp]
theorem pi.one_apply {I : Type u} {f : I → Type v₁} (i : I) [Π (i : I), has_one (f i)] :
1 i = 1
source
theorem pi.one_def {I : Type u} {f : I → Type v₁} [Π (i : I), has_one (f i)] :
1 = λ (i : I), 1
source
theorem pi.zero_def {I : Type u} {f : I → Type v₁} [Π (i : I), has_zero (f i)] :
0 = λ (i : I), 0
source
@[protected, instance]
def pi.has_mul {I : Type u} {f : I → Type v₁} [Π (i : I), has_mul (f i)] :
has_mul (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.has_add {I : Type u} {f : I → Type v₁} [Π (i : I), has_add (f i)] :
has_add (Π (i : I), f i)
source
@[simp]
theorem pi.add_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_add (f i)] :
(x + y) i = x i + y i
source
@[simp]
theorem pi.mul_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_mul (f i)] :
(x * y) i = (x i) * y i
source
theorem pi.mul_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_mul (f i)] :
x * y = λ (i : I), (x i) * y i
source
theorem pi.add_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_add (f i)] :
x + y = λ (i : I), x i + y i
source
@[protected, instance]
def pi.has_inv {I : Type u} {f : I → Type v₁} [Π (i : I), has_inv (f i)] :
has_inv (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.has_neg {I : Type u} {f : I → Type v₁} [Π (i : I), has_neg (f i)] :
has_neg (Π (i : I), f i)
source
@[simp]
theorem pi.neg_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_neg (f i)] :
(-x) i = -x i
source
@[simp]
theorem pi.inv_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_inv (f i)] :
x⁻¹ i = (x i)⁻¹
source
@[protected, instance]
def pi.has_sub {I : Type u} {f : I → Type v₁} [Π (i : I), has_sub (f i)] :
has_sub (Π (i : I), f i)
source
@[protected, instance]
def pi.has_div {I : Type u} {f : I → Type v₁} [Π (i : I), has_div (f i)] :
has_div (Π (i : I), f i)
Equations
source
@[simp]
theorem pi.div_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_div (f i)] :
(x / y) i = x i / y i
source
@[simp]
theorem pi.sub_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_sub (f i)] :
(x - y) i = x i - y i
source
theorem pi.div_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_div (f i)] :
x / y = λ (i : I), x i / y i
source
theorem pi.sub_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_sub (f i)] :
x - y = λ (i : I), x i - y i
source
def pi.single {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) (i_1 : I) :
f i_1

The function supported at i, with value x there.

Equations
source
@[simp]
theorem pi.single_eq_same {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) :
pi.single i x i = x
source
@[simp]
theorem pi.single_eq_of_ne {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {i i' : I} (h : i' ≠ i) (x : f i) :
pi.single i x i' = 0
source
@[simp]
theorem pi.single_zero {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
pi.single i 0 = 0
source
theorem pi.apply_single {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [decidable_eq I] [Π (i : I), has_zero (f i)] [Π (i : I), has_zero (g i)] (f' : Π (i : I), f i → g i) (hf' : ∀ (i : I), f' i 0 = 0) (i : I) (x : f i) (j : I) :
f' j (pi.single i x j) = pi.single i (f' i x) j
source
theorem pi.apply_single₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [decidable_eq I] [Π (i : I), has_zero (f i)] [Π (i : I), has_zero (g i)] [Π (i : I), has_zero (h i)] (f' : Π (i : I), f i → g i → h i) (hf' : ∀ (i : I), f' i 0 0 = 0) (i : I) (x : f i) (y : g i) (j : I) :
f' j (pi.single i x j) (pi.single i y j) = pi.single i (f' i x y) j
source
theorem pi.single_op {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {g : I → Type u_1} [Π (i : I), has_zero (g i)] (op : Π (i : I), f i → g i) (h : ∀ (i : I), op i 0 = 0) (i : I) (x : f i) :
pi.single i (op i x) = λ (j : I), op j (pi.single i x j)
source
theorem pi.single_op₂ {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {g₁ : I → Type u_1} {g₂ : I → Type u_2} [Π (i : I), has_zero (g₁ i)] [Π (i : I), has_zero (g₂ i)] (op : Π (i : I), g₁ i → g₂ i → f i) (h : ∀ (i : I), op i 0 0 = 0) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
pi.single i (op i x₁ x₂) = λ (j : I), op j (pi.single i x₁ j) (pi.single i x₂ j)
source
theorem pi.single_injective {I : Type u} (f : I → Type v₁) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
function.injective (pi.single i)
source
theorem subsingleton.pi_single_eq {I : Type u} {α : Type u_1} [decidable_eq I] [subsingleton I] [has_zero α] (i : I) (x : α) :
pi.single i x = λ (_x : I), x