Declarations about finitely supported functions whose support is an Option type p

Main declarations

• Finsupp.some: restrict a finitely supported function on Option α to a finitely supported function on α.

Implementation notes

This file is a noncomputable theory and uses classical logic throughout.

def Finsupp.some {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) : α →₀ M

Restrict a finitely supported function on Option α to a finitely supported function on α.

Equations

• f.some = Finsupp.comapDomain some f ⋯

@[simp]

theorem Finsupp.some_apply {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) (a : α) : f.some a = f (Option.some a)

@[simp]

theorem Finsupp.some_zero {α : Type u_1} {M : Type u_5} [Zero M] : some 0 = 0

@[simp]

theorem Finsupp.some_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f g : Option α →₀ M) : (f + g).some = f.some + g.some

@[simp]

theorem Finsupp.some_single_none {α : Type u_1} {M : Type u_5} [Zero M] (m : M) : (single none m).some = 0

@[simp]

theorem Finsupp.some_single_some {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (m : M) : (single (Option.some a) m).some = single a m

@[simp]

theorem Finsupp.embDomain_some_some {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (x : α) : (embDomain Function.Embedding.some f) (Option.some x) = f x

@[simp]

theorem Finsupp.some_update_none {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) (a : M) : (f.update none a).some = f.some

noncomputable def Finsupp.optionEquiv {α : Type u_1} {M : Type u_5} [Zero M] : (Option α →₀ M) ≃ M × (α →₀ M)

Finsupps from Option are equivalent to pairs of an element and a Finsupp on the original type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.optionEquiv_symm_apply {α : Type u_1} {M : Type u_5} [Zero M] (P : M × (α →₀ M)) : optionEquiv.symm P = (embDomain Function.Embedding.some P.2).update none P.1

@[simp]

theorem Finsupp.optionEquiv_apply {α : Type u_1} {M : Type u_5} [Zero M] (P : Option α →₀ M) : optionEquiv P = (P none, P.some)

theorem Finsupp.eq_option_embedding_update_none_iff {α : Type u_1} {M : Type u_5} [Zero M] {n : Option α →₀ M} {m : α →₀ M} {i : M} : n = (embDomain Function.Embedding.some m).update none i ↔ n none = i ∧ n.some = m

theorem Finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [CommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 1) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) : f.prod b = b none (f none) * f.some.prod fun (a : α) => b (Option.some a)

theorem Finsupp.sum_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddCommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 0) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) : f.sum b = b none (f none) + f.some.sum fun (a : α) => b (Option.some a)

theorem Finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option α → M) : (f.sum fun (o : Option α) (r : R) => r • b o) = f none • b none + f.some.sum fun (a : α) (r : R) => r • b (Option.some a)

@[simp]

theorem Finsupp.some_embDomain_some {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) : (embDomain Function.Embedding.some f).some = f

@[simp]

theorem Finsupp.embDomain_some_none {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) : (embDomain Function.Embedding.some f) none = 0