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.
@[simp]
theorem
Pi.zero_apply
{I : Type u}
{f : I → Type v₁}
(i : I)
[inst : (i : I) → Zero (f i)]
:
OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0
@[simp]
theorem
Pi.one_apply
{I : Type u}
{f : I → Type v₁}
(i : I)
[inst : (i : I) → One (f i)]
:
OfNat.ofNat ((i : I) → f i) 1 One.toOfNat1 i = 1
@[simp]
@[simp]
@[simp]
theorem
Pi.comp_zero
{α : Type u_2}
{β : Type u_1}
{γ : Type u_3}
[inst : Zero β]
(x : β → γ)
:
x ∘ 0 = Function.const α (x 0)
@[simp]
theorem
Pi.comp_one
{α : Type u_2}
{β : Type u_1}
{γ : Type u_3}
[inst : One β]
(x : β → γ)
:
x ∘ 1 = Function.const α (x 1)
@[simp]
theorem
Pi.add_apply
{I : Type u}
{f : I → Type v₁}
(x : (i : I) → f i)
(y : (i : I) → f i)
(i : I)
[inst : (i : I) → Add (f i)]
:
(((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x y i = x i + y i
@[simp]
theorem
Pi.mul_apply
{I : Type u}
{f : I → Type v₁}
(x : (i : I) → f i)
(y : (i : I) → f i)
(i : I)
[inst : (i : I) → Mul (f i)]
:
(((i : I) → f i) * ((i : I) → f i)) ((i : I) → f i) instHMul x y i = x i * y i
@[simp]
theorem
Pi.const_add
{α : Type u_2}
{β : Type u_1}
[inst : Add β]
(a : β)
(b : β)
:
Function.const α a + Function.const α b = Function.const α (a + b)
@[simp]
theorem
Pi.const_mul
{α : Type u_2}
{β : Type u_1}
[inst : Mul β]
(a : β)
(b : β)
:
Function.const α a * Function.const α b = Function.const α (a * b)
@[simp]
theorem
Pi.vadd_const
{I : Type u}
{β : Type u_2}
{α : Type u_1}
[inst : VAdd β α]
(b : β)
(a : α)
:
b +ᵥ Function.const I a = Function.const I (b +ᵥ a)
@[simp]
theorem
Pi.smul_const
{I : Type u}
{β : Type u_2}
{α : Type u_1}
[inst : SMul β α]
(b : β)
(a : α)
:
b • Function.const I a = Function.const I (b • a)
@[simp]
theorem
Pi.const_pow
{I : Type u}
{α : Type u_1}
{β : Type u_2}
[inst : Pow α β]
(a : α)
(b : β)
:
Function.const I a ^ b = Function.const I (a ^ b)
Porting note: bit0 and bit1 are deprecated. This section can be removed entirely
(without replacement?).
@[simp]
theorem
Pi.inv_apply
{I : Type u}
{f : I → Type v₁}
(x : (i : I) → f i)
(i : I)
[inst : (i : I) → Inv (f i)]
:
((i : I) → f i)⁻¹ Pi.instInv x i = (x i)⁻¹
theorem
Pi.const_neg
{α : Type u_2}
{β : Type u_1}
[inst : Neg β]
(a : β)
:
-Function.const α a = Function.const α (-a)
theorem
Pi.const_inv
{α : Type u_2}
{β : Type u_1}
[inst : Inv β]
(a : β)
:
(Function.const α a)⁻¹ = Function.const α a⁻¹
@[simp]
theorem
Pi.sub_apply
{I : Type u}
{f : I → Type v₁}
(x : (i : I) → f i)
(y : (i : I) → f i)
(i : I)
[inst : (i : I) → Sub (f i)]
:
(((i : I) → f i) - ((i : I) → f i)) ((i : I) → f i) instHSub x y i = x i - y i
@[simp]
theorem
Pi.div_apply
{I : Type u}
{f : I → Type v₁}
(x : (i : I) → f i)
(y : (i : I) → f i)
(i : I)
[inst : (i : I) → Div (f i)]
:
(((i : I) → f i) / ((i : I) → f i)) ((i : I) → f i) instHDiv x y i = x i / y i
@[simp]
theorem
Pi.const_sub
{α : Type u_2}
{β : Type u_1}
[inst : Sub β]
(a : β)
(b : β)
:
Function.const α a - Function.const α b = Function.const α (a - b)
@[simp]
theorem
Pi.const_div
{α : Type u_2}
{β : Type u_1}
[inst : Div β]
(a : β)
(b : β)
:
Function.const α a / Function.const α b = Function.const α (a / b)
def
Pi.single
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
(i : I)
(x : f i)
(j : I)
:
f j
The function supported at i, with value x there, and 0 elsewhere.
Equations
- Pi.single i x = Function.update 0 i x
def
Pi.mulSingle
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
(i : I)
(x : f i)
(j : I)
:
f j
The function supported at i, with value x there, and 1 elsewhere.
Equations
- Pi.mulSingle i x = Function.update 1 i x
@[simp]
theorem
Pi.single_eq_same
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
(i : I)
(x : f i)
:
@[simp]
theorem
Pi.mulSingle_eq_same
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
(i : I)
(x : f i)
:
Pi.mulSingle i x i = x
@[simp]
theorem
Pi.single_eq_of_ne
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
{i : I}
{i' : I}
(h : i' ≠ i)
(x : f i)
:
@[simp]
theorem
Pi.mulSingle_eq_of_ne
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
{i : I}
{i' : I}
(h : i' ≠ i)
(x : f i)
:
Pi.mulSingle i x i' = 1
@[simp]
theorem
Pi.mulSingle_eq_of_ne'
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
{i : I}
{i' : I}
(h : i ≠ i')
(x : f i)
:
Pi.mulSingle i x i' = 1
Abbreviation for mulSingle_eq_of_ne h.symm, for ease of use by simp.
@[simp]
theorem
Pi.single_zero
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
(i : I)
:
@[simp]
theorem
Pi.mulSingle_one
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
(i : I)
:
Pi.mulSingle i 1 = 1
theorem
Pi.mulSingle_apply
{I : Type u}
{β : Type u_1}
[inst : DecidableEq I]
[inst : One β]
(i : I)
(x : β)
(i' : I)
:
Pi.mulSingle i x i' = if i' = i then x else 1
On non-dependent functions, Pi.mulSingle can be expressed as an ite
theorem
Pi.mulSingle_comm
{I : Type u}
{β : Type u_1}
[inst : DecidableEq I]
[inst : One β]
(i : I)
(x : β)
(i' : I)
:
Pi.mulSingle i x i' = Pi.mulSingle i' x i
On non-dependent functions, Pi.mulSingle is symmetric in the two indices.
theorem
Pi.apply_mulSingle
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
[inst : (i : I) → One (g i)]
(f' : (i : I) → f i → g i)
(hf' : ∀ (i : I), f' i 1 = 1)
(i : I)
(x : f i)
(j : I)
:
f' j (Pi.mulSingle i x j) = Pi.mulSingle i (f' i x) j
theorem
Pi.apply_single₂
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{h : I → Type v₃}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
[inst : (i : I) → Zero (g i)]
[inst : (i : I) → 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)
:
theorem
Pi.apply_mulSingle₂
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{h : I → Type v₃}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
[inst : (i : I) → One (g i)]
[inst : (i : I) → One (h i)]
(f' : (i : I) → f i → g i → h i)
(hf' : ∀ (i : I), f' i 1 1 = 1)
(i : I)
(x : f i)
(y : g i)
(j : I)
:
f' j (Pi.mulSingle i x j) (Pi.mulSingle i y j) = Pi.mulSingle i (f' i x y) j
theorem
Pi.mulSingle_op
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
{g : I → Type u_1}
[inst : (i : I) → One (g i)]
(op : (i : I) → f i → g i)
(h : ∀ (i : I), op i 1 = 1)
(i : I)
(x : f i)
:
Pi.mulSingle i (op i x) = fun j => op j (Pi.mulSingle i x j)
theorem
Pi.single_op₂
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
{g₁ : I → Type u_1}
{g₂ : I → Type u_2}
[inst : (i : I) → Zero (g₁ i)]
[inst : (i : I) → 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)
:
theorem
Pi.mulSingle_op₂
{I : Type u}
{f : I → Type v₁}
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
{g₁ : I → Type u_1}
{g₂ : I → Type u_2}
[inst : (i : I) → One (g₁ i)]
[inst : (i : I) → One (g₂ i)]
(op : (i : I) → g₁ i → g₂ i → f i)
(h : ∀ (i : I), op i 1 1 = 1)
(i : I)
(x₁ : g₁ i)
(x₂ : g₂ i)
:
Pi.mulSingle i (op i x₁ x₂) = fun j => op j (Pi.mulSingle i x₁ j) (Pi.mulSingle i x₂ j)
theorem
Pi.single_injective
{I : Type u}
(f : I → Type v₁)
[inst : DecidableEq I]
[inst : (i : I) → Zero (f i)]
(i : I)
:
theorem
Pi.mulSingle_injective
{I : Type u}
(f : I → Type v₁)
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
(i : I)
:
@[simp]
theorem
Pi.mulSingle_inj
{I : Type u}
(f : I → Type v₁)
[inst : DecidableEq I]
[inst : (i : I) → One (f i)]
(i : I)
{x : f i}
{y : f i}
:
Pi.mulSingle i x = Pi.mulSingle i y ↔ x = y
theorem
Function.extend_zero
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Zero γ]
(f : α → β)
:
Function.extend f 0 0 = 0
theorem
Function.extend_one
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : One γ]
(f : α → β)
:
Function.extend f 1 1 = 1
theorem
Function.extend_add
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Add γ]
(f : α → β)
(g₁ : α → γ)
(g₂ : α → γ)
(e₁ : β → γ)
(e₂ : β → γ)
:
Function.extend f (g₁ + g₂) (e₁ + e₂) = Function.extend f g₁ e₁ + Function.extend f g₂ e₂
theorem
Function.extend_mul
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Mul γ]
(f : α → β)
(g₁ : α → γ)
(g₂ : α → γ)
(e₁ : β → γ)
(e₂ : β → γ)
:
Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂
theorem
Function.extend_neg
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Neg γ]
(f : α → β)
(g : α → γ)
(e : β → γ)
:
Function.extend f (-g) (-e) = -Function.extend f g e
theorem
Function.extend_inv
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Inv γ]
(f : α → β)
(g : α → γ)
(e : β → γ)
:
Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹
theorem
Function.extend_sub
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Sub γ]
(f : α → β)
(g₁ : α → γ)
(g₂ : α → γ)
(e₁ : β → γ)
(e₂ : β → γ)
:
Function.extend f (g₁ - g₂) (e₁ - e₂) = Function.extend f g₁ e₁ - Function.extend f g₂ e₂
theorem
Function.extend_div
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Div γ]
(f : α → β)
(g₁ : α → γ)
(g₂ : α → γ)
(e₁ : β → γ)
(e₂ : β → γ)
:
Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂
theorem
Function.surjective_pi_map
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{F : (i : I) → f i → g i}
(hF : ∀ (i : I), Function.Surjective (F i))
:
Function.Surjective fun x i => F i (x i)
theorem
Function.injective_pi_map
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{F : (i : I) → f i → g i}
(hF : ∀ (i : I), Function.Injective (F i))
:
Function.Injective fun x i => F i (x i)
theorem
Function.bijective_pi_map
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{F : (i : I) → f i → g i}
(hF : ∀ (i : I), Function.Bijective (F i))
:
Function.Bijective fun x i => F i (x i)
def
uniqueOfSurjectiveZero
(α : Type u_1)
{β : Type u_2}
[inst : Zero β]
(h : Function.Surjective 0)
:
Unique β
If the zero function is surjective, the codomain is trivial.
Equations
def
uniqueOfSurjectiveOne
(α : Type u_1)
{β : Type u_2}
[inst : One β]
(h : Function.Surjective 1)
:
Unique β
If the one function is surjective, the codomain is trivial.
Equations
theorem
Subsingleton.pi_single_eq
{I : Type u}
{α : Type u_1}
[inst : DecidableEq I]
[inst : Subsingleton I]
[inst : Zero α]
(i : I)
(x : α)
:
theorem
Subsingleton.pi_mulSingle_eq
{I : Type u}
{α : Type u_1}
[inst : DecidableEq I]
[inst : Subsingleton I]
[inst : One α]
(i : I)
(x : α)
:
Pi.mulSingle i x = fun x => x
@[simp]
theorem
Sum.elim_single_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : DecidableEq α]
[inst : DecidableEq β]
[inst : Zero γ]
(i : α)
(c : γ)
:
@[simp]
theorem
Sum.elim_mulSingle_one
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : DecidableEq α]
[inst : DecidableEq β]
[inst : One γ]
(i : α)
(c : γ)
:
Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (Sum.inl i) c
@[simp]
theorem
Sum.elim_zero_single
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : DecidableEq α]
[inst : DecidableEq β]
[inst : Zero γ]
(i : β)
(c : γ)
:
@[simp]
theorem
Sum.elim_one_mulSingle
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : DecidableEq α]
[inst : DecidableEq β]
[inst : One γ]
(i : β)
(c : γ)
:
Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c