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]
Equations
- pi.has_one = {one := λ (_x : I), 1}
@[simp]
@[simp]
@[instance]
Equations
- pi.has_mul = {mul := λ (f_1 g : Π (i : I), f i) (i : I), (f_1 i) * g i}
@[instance]
@[instance]
Equations
- pi.has_inv = {inv := λ (f_1 : Π (i : I), f i) (i : I), (f_1 i)⁻¹}
@[instance]
@[instance]
@[instance]
Equations
- pi.has_div = {div := λ (f_1 g : Π (i : I), f i) (i : I), f_1 i / g 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
- pi.single i x = function.update 0 i x
@[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) :
@[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) :
theorem
pi.single_injective
{I : Type u}
(f : I → Type v)
[decidable_eq I]
[Π (i : I), has_zero (f i)]
(i : I) :