Instances and theorems on pi types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
@[simp]
@[simp]
theorem
pi.comp_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
(x : β → γ) :
x ∘ 0 = function.const α (x 0)
@[simp]
theorem
pi.comp_one
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_one β]
(x : β → γ) :
x ∘ 1 = function.const α (x 1)
@[simp]
theorem
pi.const_add
{α : Type u_1}
{β : Type u_2}
[has_add β]
(a b : β) :
function.const α a + function.const α b = function.const α (a + b)
@[simp]
theorem
pi.const_mul
{α : Type u_1}
{β : Type u_2}
[has_mul β]
(a b : β) :
function.const α a * function.const α b = function.const α (a * b)
@[simp]
theorem
pi.vadd_const
{I : Type u}
{α : Type u_1}
{β : Type u_2}
[has_vadd α β]
(a : α)
(b : β) :
a +ᵥ function.const I b = function.const I (a +ᵥ b)
@[simp]
theorem
pi.smul_const
{I : Type u}
{α : Type u_1}
{β : Type u_2}
[has_smul α β]
(a : α)
(b : β) :
a • function.const I b = function.const I (a • b)
@[simp]
theorem
pi.const_pow
{I : Type u}
{α : Type u_1}
{β : Type u_2}
[has_pow β α]
(b : β)
(a : α) :
function.const I b ^ a = function.const I (b ^ a)
theorem
pi.const_inv
{α : Type u_1}
{β : Type u_2}
[has_inv β]
(a : β) :
(function.const α a)⁻¹ = function.const α a⁻¹
theorem
pi.const_neg
{α : Type u_1}
{β : Type u_2}
[has_neg β]
(a : β) :
-function.const α a = function.const α (-a)
@[simp]
theorem
pi.const_sub
{α : Type u_1}
{β : Type u_2}
[has_sub β]
(a b : β) :
function.const α a - function.const α b = function.const α (a - b)
@[simp]
theorem
pi.const_div
{α : Type u_1}
{β : Type u_2}
[has_div β]
(a b : β) :
function.const α a / function.const α b = function.const α (a / b)
def
pi.mul_single
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
(i : I)
(x : f i)
(i_1 : I) :
f i_1
The function supported at i, with value x there, and 1 elsewhere.
Equations
- pi.mul_single i x = function.update 1 i x
@[simp]
theorem
pi.mul_single_eq_same
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
(i : I)
(x : f i) :
pi.mul_single i x 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.mul_single_eq_of_ne
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
{i i' : I}
(h : i' ≠ i)
(x : f i) :
pi.mul_single i x i' = 1
@[simp]
theorem
pi.mul_single_eq_of_ne'
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
{i i' : I}
(h : i ≠ i')
(x : f i) :
pi.mul_single i x i' = 1
Abbreviation for mul_single_eq_of_ne h.symm, for ease of use by simp.
@[simp]
theorem
pi.single_zero
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_zero (f i)]
(i : I) :
@[simp]
theorem
pi.mul_single_one
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
(i : I) :
pi.mul_single i 1 = 1
theorem
pi.mul_single_apply
{I : Type u}
[decidable_eq I]
{β : Type u_1}
[has_one β]
(i : I)
(x : β)
(i' : I) :
pi.mul_single i x i' = ite (i' = i) x 1
On non-dependent functions, pi.mul_single can be expressed as an ite
theorem
pi.single_comm
{I : Type u}
[decidable_eq I]
{β : Type u_1}
[has_zero β]
(i : I)
(x : β)
(i' : I) :
On non-dependent functions, pi.single is symmetric in the two
indices.
theorem
pi.mul_single_comm
{I : Type u}
[decidable_eq I]
{β : Type u_1}
[has_one β]
(i : I)
(x : β)
(i' : I) :
pi.mul_single i x i' = pi.mul_single i' x i
On non-dependent functions, pi.mul_single is symmetric in the two indices.
theorem
pi.apply_mul_single
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
[decidable_eq I]
[Π (i : I), has_one (f i)]
[Π (i : I), has_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.mul_single i x j) = pi.mul_single i (f' i x) j
theorem
pi.apply_mul_single₂
{I : Type u}
{f : I → Type v₁}
{g : I → Type v₂}
{h : I → Type v₃}
[decidable_eq I]
[Π (i : I), has_one (f i)]
[Π (i : I), has_one (g i)]
[Π (i : I), has_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.mul_single i x j) (pi.mul_single i y j) = pi.mul_single i (f' i x y) j
theorem
pi.mul_single_op
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
{g : I → Type u_1}
[Π (i : I), has_one (g i)]
(op : Π (i : I), f i → g i)
(h : ∀ (i : I), op i 1 = 1)
(i : I)
(x : f i) :
pi.mul_single i (op i x) = λ (j : I), op j (pi.mul_single i x j)
theorem
pi.mul_single_op₂
{I : Type u}
{f : I → Type v₁}
[decidable_eq I]
[Π (i : I), has_one (f i)]
{g₁ : I → Type u_1}
{g₂ : I → Type u_2}
[Π (i : I), has_one (g₁ i)]
[Π (i : I), has_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.mul_single i (op i x₁ x₂) = λ (j : I), op j (pi.mul_single i x₁ j) (pi.mul_single i x₂ j)
theorem
pi.mul_single_injective
{I : Type u}
(f : I → Type v₁)
[decidable_eq I]
[Π (i : I), has_one (f i)]
(i : I) :
theorem
pi.single_injective
{I : Type u}
(f : I → Type v₁)
[decidable_eq I]
[Π (i : I), has_zero (f i)]
(i : I) :
@[simp]
theorem
pi.mul_single_inj
{I : Type u}
(f : I → Type v₁)
[decidable_eq I]
[Π (i : I), has_one (f i)]
(i : I)
{x y : f i} :
pi.mul_single i x = pi.mul_single i y ↔ x = y
theorem
function.extend_one
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_one γ]
(f : α → β) :
function.extend f 1 1 = 1
theorem
function.extend_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero γ]
(f : α → β) :
function.extend f 0 0 = 0
theorem
function.extend_add
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_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_1}
{β : Type u_2}
{γ : Type u_3}
[has_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_1}
{β : Type u_2}
{γ : Type u_3}
[has_neg γ]
(f : α → β)
(g : α → γ)
(e : β → γ) :
function.extend f (-g) (-e) = -function.extend f g e
theorem
function.extend_inv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_inv γ]
(f : α → β)
(g : α → γ)
(e : β → γ) :
function.extend f g⁻¹ e⁻¹ = (function.extend f g e)⁻¹
theorem
function.extend_div
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_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.extend_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_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.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 (λ (x : Π (i : I), f i) (i : 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 (λ (x : Π (i : I), f i) (i : 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 (λ (x : Π (i : I), f i) (i : I), F i (x i))
def
unique_of_surjective_one
(α : Type u_1)
{β : Type u_2}
[has_one β]
(h : function.surjective 1) :
unique β
If the one function is surjective, the codomain is trivial.
Equations
def
unique_of_surjective_zero
(α : Type u_1)
{β : Type u_2}
[has_zero β]
(h : function.surjective 0) :
unique β
If the zero function is surjective, the codomain is trivial.
Equations
theorem
subsingleton.pi_mul_single_eq
{I : Type u}
{α : Type u_1}
[decidable_eq I]
[subsingleton I]
[has_one α]
(i : I)
(x : α) :
pi.mul_single i x = λ (_x : I), x
theorem
subsingleton.pi_single_eq
{I : Type u}
{α : Type u_1}
[decidable_eq I]
[subsingleton I]
[has_zero α]
(i : I)
(x : α) :
@[simp]
theorem
sum.elim_single_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
[decidable_eq β]
[has_zero γ]
(i : α)
(c : γ) :
@[simp]
theorem
sum.elim_mul_single_one
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
[decidable_eq β]
[has_one γ]
(i : α)
(c : γ) :
sum.elim (pi.mul_single i c) 1 = pi.mul_single (sum.inl i) c
@[simp]
theorem
sum.elim_zero_single
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
[decidable_eq β]
[has_zero γ]
(i : β)
(c : γ) :
@[simp]
theorem
sum.elim_one_mul_single
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
[decidable_eq β]
[has_one γ]
(i : β)
(c : γ) :
sum.elim 1 (pi.mul_single i c) = pi.mul_single (sum.inr i) c