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 Pi.instZero {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : Zero ((i : I) → f i)

Equations

• Pi.instZero = { zero := fun x => 0 }

instance Pi.instOne {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : One ((i : I) → f i)

Equations

• Pi.instOne = { one := fun x => 1 }

@[simp]

theorem Pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [(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) [(i : I) → One (f i)] : OfNat.ofNat ((i : I) → f i) 1 One.toOfNat1 i = 1

theorem Pi.zero_def {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : 0 = fun x => 0

theorem Pi.one_def {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : 1 = fun x => 1

@[simp]

theorem Pi.const_zero {α : Type u_1} {β : Type u_2} [Zero β] : Function.const α 0 = 0

@[simp]

theorem Pi.const_one {α : Type u_1} {β : Type u_2} [One β] : Function.const α 1 = 1

@[simp]

theorem Pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (x : α → β) : 0 ∘ x = 0

@[simp]

theorem Pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (x : α → β) : 1 ∘ x = 1

@[simp]

theorem Pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] (x : β → γ) : x ∘ 0 = Function.const α (x 0)

@[simp]

theorem Pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] (x : β → γ) : x ∘ 1 = Function.const α (x 1)

instance Pi.instAdd {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] : Add ((i : I) → f i)

Equations

• Pi.instAdd = { add := fun f g i => f i + g i }

instance Pi.instMul {I : Type u} {f : I → Type v₁} [(i : I) → Mul (f i)] : Mul ((i : I) → f i)

Equations

• Pi.instMul = { mul := fun f g i => f i * g i }

@[simp]

theorem Pi.add_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(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) [(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

theorem Pi.add_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Add (f i)] : x + y = fun i => x i + y i

theorem Pi.mul_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Mul (f i)] : x * y = fun i => x i * y i

@[simp]

theorem Pi.const_add {α : Type u_1} {β : Type u_2} [Add β] (a : β) (b : β) : Function.const α a + Function.const α b = Function.const α (a + b)

@[simp]

theorem Pi.const_mul {α : Type u_1} {β : Type u_2} [Mul β] (a : β) (b : β) : Function.const α a * Function.const α b = Function.const α (a * b)

theorem Pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (x : β → γ) (y : β → γ) (z : α → β) : (x + y) ∘ z = x ∘ z + y ∘ z

theorem Pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (x : β → γ) (y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z

instance Pi.instVAdd {I : Type u} {α : Type u_1} {f : I → Type v₁} [(i : I) → VAdd α (f i)] : VAdd α ((i : I) → f i)

Equations

• Pi.instVAdd = { vadd := fun s x i => s +ᵥ x i }

instance Pi.instSMul {I : Type u} {α : Type u_1} {f : I → Type v₁} [(i : I) → SMul α (f i)] : SMul α ((i : I) → f i)

Equations

• Pi.instSMul = { smul := fun s x i => s • x i }

instance Pi.instPow {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] : Pow ((i : I) → f i) β

Equations

• Pi.instPow = { pow := fun x b i => x i ^ b }

@[simp]

theorem Pi.smul_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) (i : I) : (β • ((i : I) → f i)) ((i : I) → f i) instHSMul b x i = b • x i

@[simp]

theorem Pi.vadd_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) (i : I) : (β +ᵥ ((i : I) → f i)) ((i : I) → f i) instHVAdd b x i = b +ᵥ x i

@[simp]

theorem Pi.pow_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) (i : I) : (((i : I) → f i) ^ β) ((i : I) → f i) instHPow x b i = x i ^ b

theorem Pi.smul_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) : b • x = fun i => b • x i

theorem Pi.vadd_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) : b +ᵥ x = fun i => b +ᵥ x i

theorem Pi.pow_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) : x ^ b = fun i => x i ^ b

@[simp]

theorem Pi.vadd_const {I : Type u} {β : Type u_2} {α : Type u_1} [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} [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} [Pow α β] (a : α) (b : β) : Function.const I a ^ b = Function.const I (a ^ b)

theorem Pi.vadd_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] (a : α) (x : β → γ) (y : I → β) : (a +ᵥ x) ∘ y = a +ᵥ x ∘ y

theorem Pi.smul_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α γ] (a : α) (x : β → γ) (y : I → β) : (a • x) ∘ y = a • x ∘ y

theorem Pi.pow_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a

Porting note: bit0 and bit1 are deprecated. This section can be removed entirely (without replacement?).

@[simp, deprecated]

theorem Pi.bit0_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Add (f i)] : bit0 ((i : I) → f i) Pi.instAdd x i = bit0 (x i)

@[simp, deprecated]

theorem Pi.bit1_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Add (f i)] [(i : I) → One (f i)] : bit1 ((i : I) → f i) Pi.instOne Pi.instAdd x i = bit1 (x i)

instance Pi.instNeg {I : Type u} {f : I → Type v₁} [(i : I) → Neg (f i)] : Neg ((i : I) → f i)

Equations

• Pi.instNeg = { neg := fun f i => -f i }

instance Pi.instInv {I : Type u} {f : I → Type v₁} [(i : I) → Inv (f i)] : Inv ((i : I) → f i)

Equations

• Pi.instInv = { inv := fun f i => (f i)⁻¹ }

@[simp]

theorem Pi.neg_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Neg (f i)] : (-((i : I) → f i)) Pi.instNeg x i = -x i

@[simp]

theorem Pi.inv_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Inv (f i)] : ((i : I) → f i)⁻¹ Pi.instInv x i = (x i)⁻¹

theorem Pi.neg_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Neg (f i)] : -x = fun i => -x i

theorem Pi.inv_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Inv (f i)] : x⁻¹ = fun i => (x i)⁻¹

theorem Pi.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) : -Function.const α a = Function.const α (-a)

theorem Pi.const_inv {α : Type u_1} {β : Type u_2} [Inv β] (a : β) : (Function.const α a)⁻¹ = Function.const α a⁻¹

theorem Pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (x : β → γ) (y : α → β) : (-x) ∘ y = -x ∘ y

theorem Pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹

instance Pi.instSub {I : Type u} {f : I → Type v₁} [(i : I) → Sub (f i)] : Sub ((i : I) → f i)

Equations

• Pi.instSub = { sub := fun f g i => f i - g i }

instance Pi.instDiv {I : Type u} {f : I → Type v₁} [(i : I) → Div (f i)] : Div ((i : I) → f i)

Equations

• Pi.instDiv = { div := fun f g i => f i / g i }

@[simp]

theorem Pi.sub_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(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) [(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

theorem Pi.sub_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Sub (f i)] : x - y = fun i => x i - y i

theorem Pi.div_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Div (f i)] : x / y = fun i => x i / y i

theorem Pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (x : β → γ) (y : β → γ) (z : α → β) : (x - y) ∘ z = x ∘ z - y ∘ z

theorem Pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (x : β → γ) (y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z

@[simp]

theorem Pi.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a : β) (b : β) : Function.const α a - Function.const α b = Function.const α (a - b)

@[simp]

theorem Pi.const_div {α : Type u_1} {β : Type u_2} [Div β] (a : β) (b : β) : Function.const α a / Function.const α b = Function.const α (a / b)

def Pi.single {I : Type u} {f : I → Type v₁} [DecidableEq I] [(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₁} [DecidableEq I] [(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₁} [DecidableEq I] [(i : I) → Zero (f i)] (i : I) (x : f i) : Pi.single i x i = x

@[simp]

theorem Pi.mulSingle_eq_same {I : Type u} {f : I → Type v₁} [DecidableEq I] [(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₁} [DecidableEq I] [(i : I) → Zero (f i)] {i : I} {i' : I} (h : i' ≠ i) (x : f i) : Pi.single i x i' = 0

@[simp]

theorem Pi.mulSingle_eq_of_ne {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {i : I} {i' : I} (h : i' ≠ i) (x : f i) : Pi.mulSingle i x i' = 1

@[simp]

theorem Pi.single_eq_of_ne' {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {i : I} {i' : I} (h : i ≠ i') (x : f i) : Pi.single i x i' = 0

Abbreviation for single_eq_of_ne h.symm, for ease of use by simp.

@[simp]

theorem Pi.mulSingle_eq_of_ne' {I : Type u} {f : I → Type v₁} [DecidableEq I] [(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₁} [DecidableEq I] [(i : I) → Zero (f i)] (i : I) : Pi.single i 0 = 0

@[simp]

theorem Pi.mulSingle_one {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] (i : I) : Pi.mulSingle i 1 = 1

theorem Pi.single_apply {I : Type u} {β : Type u_2} [DecidableEq I] [Zero β] (i : I) (x : β) (i' : I) : Pi.single i x i' = if i' = i then x else 0

On non-dependent functions, Pi.single can be expressed as an ite

theorem Pi.mulSingle_apply {I : Type u} {β : Type u_2} [DecidableEq I] [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.single_comm {I : Type u} {β : Type u_2} [DecidableEq I] [Zero β] (i : I) (x : β) (i' : I) : Pi.single i x i' = Pi.single i' x i

On non-dependent functions, Pi.single is symmetric in the two indices.

theorem Pi.mulSingle_comm {I : Type u} {β : Type u_2} [DecidableEq I] [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_single {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [DecidableEq I] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] (f' : (i : I) → f i → g i) (hf' : ∀ (i : I), f' i 0 = 0) (i : I) (x : f i) (j : I) : f' j (Pi.single i x j) = Pi.single i (f' i x) j

theorem Pi.apply_mulSingle {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [DecidableEq I] [(i : I) → One (f i)] [(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₃} [DecidableEq I] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] [(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) : f' j (Pi.single i x j) (Pi.single i y j) = Pi.single i (f' i x y) j

theorem Pi.apply_mulSingle₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [DecidableEq I] [(i : I) → One (f i)] [(i : I) → One (g i)] [(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.single_op {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {g : I → Type u_4} [(i : I) → Zero (g i)] (op : (i : I) → f i → g i) (h : ∀ (i : I), op i 0 = 0) (i : I) (x : f i) : Pi.single i (op i x) = fun j => op j (Pi.single i x j)

theorem Pi.mulSingle_op {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {g : I → Type u_4} [(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₁} [DecidableEq I] [(i : I) → Zero (f i)] {g₁ : I → Type u_4} {g₂ : I → Type u_5} [(i : I) → Zero (g₁ i)] [(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) : Pi.single i (op i x₁ x₂) = fun j => op j (Pi.single i x₁ j) (Pi.single i x₂ j)

theorem Pi.mulSingle_op₂ {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {g₁ : I → Type u_4} {g₂ : I → Type u_5} [(i : I) → One (g₁ i)] [(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₁) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) : Function.Injective (Pi.single i)

theorem Pi.mulSingle_injective {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → One (f i)] (i : I) : Function.Injective (Pi.mulSingle i)

@[simp]

theorem Pi.single_inj {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) {x : f i} {y : f i} : Pi.single i x = Pi.single i y ↔ x = y

@[simp]

theorem Pi.mulSingle_inj {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → One (f i)] (i : I) {x : f i} {y : f i} : Pi.mulSingle i x = Pi.mulSingle i y ↔ x = y

def Pi.prod {I : Type u} {f : I → Type v₁} {g : I → Type v₂} (f' : (i : I) → f i) (g' : (i : I) → g i) (i : I) : f i × g i

The mapping into a product type built from maps into each component.

Equations

• Pi.prod f' g' i = (f' i, g' i)

theorem Pi.prod_fst_snd {α : Type u_1} {β : Type u_2} : Pi.prod Prod.fst Prod.snd = id

theorem Pi.prod_snd_fst {α : Type u_1} {β : Type u_2} : Pi.prod Prod.snd Prod.fst = Prod.swap

theorem Function.extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (f : α → β) : Function.extend f 0 0 = 0

theorem Function.extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (f : α → β) : Function.extend f 1 1 = 1

theorem Function.extend_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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} [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} [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} [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) : Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹

theorem Function.extend_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} {γ : Type u_3} [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_4) {β : Type u_5} [Zero β] (h : Function.Surjective 0) : Unique β

If the zero function is surjective, the codomain is trivial.

Equations

• uniqueOfSurjectiveZero α h = Function.Surjective.uniqueOfSurjectiveConst α 0 h

def uniqueOfSurjectiveOne (α : Type u_4) {β : Type u_5} [One β] (h : Function.Surjective 1) : Unique β

If the one function is surjective, the codomain is trivial.

Equations

• uniqueOfSurjectiveOne α h = Function.Surjective.uniqueOfSurjectiveConst α 1 h

theorem Subsingleton.pi_single_eq {I : Type u} {α : Type u_4} [DecidableEq I] [Subsingleton I] [Zero α] (i : I) (x : α) : Pi.single i x = fun x => x

theorem Subsingleton.pi_mulSingle_eq {I : Type u} {α : Type u_4} [DecidableEq I] [Subsingleton I] [One α] (i : I) (x : α) : Pi.mulSingle i x = fun x => x

@[simp]

theorem Sum.elim_zero_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] : Sum.elim 0 0 = 0

@[simp]

theorem Sum.elim_one_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] : Sum.elim 1 1 = 1

@[simp]

theorem Sum.elim_single_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [Zero γ] (i : α) (c : γ) : Sum.elim (Pi.single i c) 0 = Pi.single (Sum.inl i) c

@[simp]

theorem Sum.elim_mulSingle_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [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} [DecidableEq α] [DecidableEq β] [Zero γ] (i : β) (c : γ) : Sum.elim 0 (Pi.single i c) = Pi.single (Sum.inr i) c

@[simp]

theorem Sum.elim_one_mulSingle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) : Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c

theorem Sum.elim_neg_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [Neg γ] : Sum.elim (-a) (-b) = -Sum.elim a b

theorem Sum.elim_inv_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [Inv γ] : Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹

theorem Sum.elim_add_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (a' : α → γ) (b : β → γ) (b' : β → γ) [Add γ] : Sum.elim (a + a') (b + b') = Sum.elim a b + Sum.elim a' b'

theorem Sum.elim_mul_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (a' : α → γ) (b : β → γ) (b' : β → γ) [Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

theorem Sum.elim_sub_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (a' : α → γ) (b : β → γ) (b' : β → γ) [Sub γ] : Sum.elim (a - a') (b - b') = Sum.elim a b - Sum.elim a' b'

theorem Sum.elim_div_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (a' : α → γ) (b : β → γ) (b' : β → γ) [Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'