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

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

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

pi.has_one = {one := λ (_x : I), 1}

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

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

pi.has_mul = {mul := λ (f_1 g : Π (i : I), f i) (i : I), (f_1 i) * g i}

source

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

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

pi.has_inv = {inv := λ (f_1 : Π (i : I), f i) (i : I), (f_1 i)⁻¹}

source

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

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

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

pi.has_div = {div := λ (f_1 g : Π (i : I), f i) (i : I), f_1 i / g i}

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

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

pi.single i x = function.update 0 i x

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

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)