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.
Porting note: bit0
and bit1
are deprecated. This section can be removed entirely
(without replacement?).
The function supported at i
, with value x
there, and 0
elsewhere.
Equations
- Pi.single i x = Function.update 0 i x
The function supported at i
, with value x
there, and 1
elsewhere.
Equations
- Pi.mulSingle i x = Function.update 1 i x
Abbreviation for mulSingle_eq_of_ne h.symm
, for ease of use by simp
.
On non-dependent functions, Pi.mulSingle
can be expressed as an ite
On non-dependent functions, Pi.mulSingle
is symmetric in the two indices.
If the zero function is surjective, the codomain is trivial.
Equations
If the one function is surjective, the codomain is trivial.