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.

@[instance]
def pi.has_zero {I : Type u} {f : I → Type v} [Π (i : I), has_zero (f i)] :
has_zero (Π (i : I), f i)

@[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
@[simp]
theorem pi.zero_apply {I : Type u} {f : I → Type v} (i : I) [Π (i : I), has_zero (f i)] :
0 i = 0

@[simp]
theorem pi.one_apply {I : Type u} {f : I → Type v} (i : I) [Π (i : I), has_one (f i)] :
1 i = 1

theorem pi.one_def {I : Type u} {f : I → Type v} [Π (i : I), has_one (f i)] :
1 = λ (i : I), 1

theorem pi.zero_def {I : Type u} {f : I → Type v} [Π (i : I), has_zero (f i)] :
0 = λ (i : I), 0

@[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
@[instance]
def pi.has_add {I : Type u} {f : I → Type v} [Π (i : I), has_add (f i)] :
has_add (Π (i : I), f i)

@[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

@[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

@[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
@[instance]
def pi.has_neg {I : Type u} {f : I → Type v} [Π (i : I), has_neg (f i)] :
has_neg (Π (i : I), f i)

@[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

@[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)⁻¹

@[instance]
def pi.has_sub {I : Type u} {f : I → Type v} [Π (i : I), has_sub (f i)] :
has_sub (Π (i : I), f i)

@[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
@[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

@[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

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
@[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

@[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

theorem pi.single_injective {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :