Mathlib.Data.Finsupp.Single

Finsupp.single definition

(a : α) (b : M) : α →₀ M

Full source

/-- `single a b` is the finitely supported function with value `b` at `a` and zero otherwise. -/
def single (a : α) (b : M) : α →₀ M where
  support :=
    haveI := Classical.decEq M
    if b = 0 then ∅ else {a}
  toFun :=
    haveI := Classical.decEq α
    Pi.single a b
  mem_support_toFun a' := by
    classical
      obtain rfl | hb := eq_or_ne b 0
      · simp [Pi.single, update]
      rw [if_neg hb, mem_singleton]
      obtain rfl | ha := eq_or_ne a' a
      · simp [hb, Pi.single, update]
      simp [Pi.single_eq_of_ne' ha.symm, ha]

Finitely supported function with single nonzero value

Informal description

The function `single a b` is the finitely supported function from `α` to `M` that takes the value `b` at `a` and zero everywhere else.

Finsupp.single_apply theorem

[Decidable (a = a')] : single a b a' = if a = a' then b else 0

Full source

theorem single_apply [Decidable (a = a')] : single a b a' = if a = a' then b else 0 := by
  classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

Evaluation of Single-Point Finitely Supported Function

Informal description

For any elements $a, a' \in \alpha$ and $b \in M$, the finitely supported function `single a b` evaluated at $a'$ is equal to $b$ if $a = a'$ and $0$ otherwise. In mathematical notation: $$(\text{single } a \, b)(a') = \begin{cases} b & \text{if } a = a' \\ 0 & \text{otherwise} \end{cases}$$

Finsupp.single_apply_left theorem

{f : α → β} (hf : Function.Injective f) (x z : α) (y : M) : single (f x) y (f z) = single x y z

Full source

theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α) (y : M) :
    single (f x) y (f z) = single x y z := by classical simp only [single_apply, hf.eq_iff]

Injective Function Preserves Single-Point Evaluation in Finitely Supported Functions

Informal description

Let $f : \alpha \to \beta$ be an injective function. For any elements $x, z \in \alpha$ and $y \in M$, the finitely supported function $\text{single}(f(x), y)$ evaluated at $f(z)$ is equal to the finitely supported function $\text{single}(x, y)$ evaluated at $z$. In mathematical notation: $$\text{single}(f(x), y)(f(z)) = \text{single}(x, y)(z)$$

Finsupp.single_eq_set_indicator theorem

: ⇑(single a b) = Set.indicator { a } fun _ => b

Full source

theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by
  classical
  ext
  simp [single_apply, Set.indicator, @eq_comm _ a]

Single-Point Finitely Supported Function as Indicator Function

Informal description

The finitely supported function `single a b` is equal to the set indicator function of the singleton set $\{a\}$ with constant value $b$. In other words, for any $x \in \alpha$, we have: $$(\text{single } a \, b)(x) = \begin{cases} b & \text{if } x = a \\ 0 & \text{otherwise} \end{cases}$$

Finsupp.single_eq_same theorem

: (single a b : α →₀ M) a = b

Full source

@[simp]
theorem single_eq_same : (single a b : α →₀ M) a = b := by
  classical exact Pi.single_eq_same (f := fun _ ↦ M) a b

Evaluation of Single-Point Finitely Supported Function at Its Support Point

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ evaluates to $b$ at $a$, i.e., $\text{single}(a, b)(a) = b$.

Finsupp.single_eq_of_ne theorem

(h : a ≠ a') : (single a b : α →₀ M) a' = 0

Full source

@[simp]
theorem single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 := by
  classical exact Pi.single_eq_of_ne' h _

Vanishing Property of Single-Point Finitely Supported Function at Distinct Points

Informal description

For any distinct elements $a$ and $a'$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ evaluates to zero at $a'$, i.e., $\text{single}(a, b)(a') = 0$.

Finsupp.single_eq_update theorem

[DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Function.update (0 : _) a b

Full source

theorem single_eq_update [DecidableEq α] (a : α) (b : M) :
    ⇑(single a b) = Function.update (0 : _) a b := by
  classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]

Single-Point Finitely Supported Function as Update of Zero Function

Informal description

For any type $\alpha$ with decidable equality and any type $M$ with a zero element, the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ is equal to the function obtained by updating the zero function at the point $a$ with the value $b$. In other words, for all $x \in \alpha$, $$(\text{single}(a, b))(x) = \begin{cases} b & \text{if } x = a \\ 0 & \text{otherwise} \end{cases}$$

Finsupp.single_eq_pi_single theorem

[DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b

Full source

theorem single_eq_pi_single [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b :=
  single_eq_update a b

Equality of Single-Point Finitely Supported Function and Pointwise Single Function

Informal description

For any type $\alpha$ with decidable equality and any type $M$ with a zero element, the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ is equal to the pointwise single function $\text{Pi.single}(a, b) : \alpha \to M$, which takes the value $b$ at $a$ and zero everywhere else. In other words, for all $x \in \alpha$, $$(\text{single}(a, b))(x) = \begin{cases} b & \text{if } x = a \\ 0 & \text{otherwise} \end{cases}$$

Finsupp.single_zero theorem

(a : α) : (single a 0 : α →₀ M) = 0

Full source

@[simp]
theorem single_zero (a : α) : (single a 0 : α →₀ M) = 0 :=
  DFunLike.coe_injective <| by
    classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Single-Point Finitely Supported Function with Zero Value is Zero Function

Informal description

For any element $a$ in a type $\alpha$ and any type $M$ with a zero element, the finitely supported function $\text{single}(a, 0)$ is equal to the zero function in $\alpha \to₀ M$.

Finsupp.single_of_single_apply theorem

(a a' : α) (b : M) : single a ((single a' b) a) = single a' (single a' b) a

Full source

theorem single_of_single_apply (a a' : α) (b : M) :
    single a ((single a' b) a) = single a' (single a' b) a := by
  classical
  rw [single_apply, single_apply]
  ext
  split_ifs with h
  · rw [h]
  · rw [zero_apply, single_apply, ite_self]

Equality of Single-Point Finitely Supported Functions with Nested Evaluation

Informal description

For any elements $a, a' \in \alpha$ and $b \in M$, the finitely supported function $\text{single}(a, (\text{single}(a', b))(a))$ is equal to $\text{single}(a', (\text{single}(a', b))(a))$. In mathematical notation: $$\text{single}(a, (\text{single}(a', b))(a)) = \text{single}(a', (\text{single}(a', b))(a))$$

Finsupp.support_single_ne_zero theorem

(a : α) (hb : b ≠ 0) : (single a b).support = { a }

Full source

theorem support_single_ne_zero (a : α) (hb : b ≠ 0) : (single a b).support = {a} :=
  if_neg hb

Support of Nonzero Single Finitely Supported Function is Singleton $\{a\}$

Informal description

For any element $a$ in a type $\alpha$ and any nonzero element $b$ in an additive monoid $M$, the support of the finitely supported function $\text{single}(a, b)$ is exactly the singleton set $\{a\}$.

Finsupp.support_single_subset theorem

: (single a b).support ⊆ { a }

Full source

theorem support_single_subset : (single a b).support ⊆ {a} := by
  classical
  simp only [single]
  split_ifs <;> [exact empty_subset _; exact Subset.refl _]

Support of Single Finitely Supported Function is Subset of Singleton

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in an additive monoid $M$, the support of the finitely supported function `single a b` is a subset of the singleton set $\{a\}$.

Finsupp.single_apply_mem theorem

(x) : single a b x ∈ ({0, b} : Set M)

Full source

theorem single_apply_mem (x) : singlesingle a b x ∈ ({0, b} : Set M) := by
  rcases em (a = x) with (rfl | hx) <;> [simp; simp [single_eq_of_ne hx]]

Range of Single-Point Finitely Supported Function is $\{0, b\}$

Informal description

For any element $x$ in a type $\alpha$, the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ evaluated at $x$ is either $0$ or $b$, i.e., $\text{single}(a, b)(x) \in \{0, b\}$.

Finsupp.range_single_subset theorem

: Set.range (single a b) ⊆ {0, b}

Full source

theorem range_single_subset : Set.rangeSet.range (single a b) ⊆ {0, b} :=
  Set.range_subset_iff.2 single_apply_mem

Range of Single-Point Finitely Supported Function is Subset of $\{0, b\}$

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the range of the finitely supported function $\text{single}(a, b) : \alpha \to₀ M$ is a subset of the set $\{0, b\}$.

Finsupp.single_injective theorem

(a : α) : Function.Injective (single a : M → α →₀ M)

Full source

/-- `Finsupp.single a b` is injective in `b`. For the statement that it is injective in `a`, see
`Finsupp.single_left_injective` -/
theorem single_injective (a : α) : Function.Injective (single a : M → α →₀ M) := fun b₁ b₂ eq => by
  have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
  rwa [single_eq_same, single_eq_same] at this

Injectivity of Single-Point Finitely Supported Function in Its Value

Informal description

For any element $a$ in a type $\alpha$, the function $\text{single}(a) : M \to (\alpha \to₀ M)$, which maps an element $b \in M$ to the finitely supported function that is $b$ at $a$ and zero elsewhere, is injective. That is, for any $b_1, b_2 \in M$, if $\text{single}(a, b_1) = \text{single}(a, b_2)$, then $b_1 = b_2$.

Finsupp.single_apply_eq_zero theorem

{a x : α} {b : M} : single a b x = 0 ↔ x = a → b = 0

Full source

theorem single_apply_eq_zero {a x : α} {b : M} : singlesingle a b x = 0 ↔ x = a → b = 0 := by
  simp [single_eq_set_indicator]

Zero Evaluation Condition for Single-Point Finitely Supported Function

Informal description

For any elements $a, x$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function $\text{single}(a, b)$ evaluates to zero at $x$ if and only if either $x \neq a$ or $b = 0$. In other words: $$\text{single}(a, b)(x) = 0 \leftrightarrow (x \neq a) \lor (b = 0)$$

Finsupp.single_apply_ne_zero theorem

{a x : α} {b : M} : single a b x ≠ 0 ↔ x = a ∧ b ≠ 0

Full source

theorem single_apply_ne_zero {a x : α} {b : M} : singlesingle a b x ≠ 0single a b x ≠ 0 ↔ x = a ∧ b ≠ 0 := by
  simp [single_apply_eq_zero]

Nonzero Condition for Single-Point Finitely Supported Function

Informal description

For any elements $a, x$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function `single a b` is nonzero at $x$ if and only if $x = a$ and $b \neq 0$. In other words, $\text{single}(a, b)(x) \neq 0 \leftrightarrow (x = a) \land (b \neq 0)$.

Finsupp.mem_support_single theorem

(a a' : α) (b : M) : a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

Full source

theorem mem_support_single (a a' : α) (b : M) : a ∈ (single a' b).supporta ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0 := by
  simp [single_apply_eq_zero, not_or]

Support Condition for Single-Point Finitely Supported Function

Informal description

For any elements $a, a'$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the element $a$ is in the support of the finitely supported function `single a' b` (i.e., the set of points where the function is nonzero) if and only if $a = a'$ and $b \neq 0$.

Finsupp.single_eq_single_iff theorem

 (a₁ a₂ : α) (b₁ b₂ : M) : single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Full source

theorem single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : M) :
    singlesingle a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 := by
  constructor
  · intro eq
    by_cases h : a₁ = a₂
    · refine Or.inl ⟨h, ?_⟩
      rwa [h, (single_injective a₂).eq_iff] at eq
    · rw [DFunLike.ext_iff] at eq
      have h₁ := eq a₁
      have h₂ := eq a₂
      simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (Ne.symm h)] at h₁ h₂
      exact Or.inr ⟨h₁, h₂.symm⟩
  · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
    · rfl
    · rw [single_zero, single_zero]

Equality Criterion for Single-Point Finitely Supported Functions

Informal description

For any elements $a_1, a_2$ in a type $\alpha$ and any elements $b_1, b_2$ in a type $M$ with a zero element, the finitely supported functions $\text{single}(a_1, b_1)$ and $\text{single}(a_2, b_2)$ are equal if and only if either: 1. $a_1 = a_2$ and $b_1 = b_2$, or 2. $b_1 = 0$ and $b_2 = 0$.

Finsupp.single_left_injective theorem

(h : b ≠ 0) : Function.Injective fun a : α => single a b

Full source

/-- `Finsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
`Finsupp.single_injective` -/
theorem single_left_injective (h : b ≠ 0) : Function.Injective fun a : α => single a b :=
  fun _a _a' H => (((single_eq_single_iff _ _ _ _).mp H).resolve_right fun hb => h hb.1).left

Injectivity of Single-Point Finitely Supported Function in First Argument for Nonzero Value

Informal description

For any nonzero element $b$ in a type $M$ with a zero element, the function $a \mapsto \text{single}(a, b)$ is injective. That is, if $\text{single}(a_1, b) = \text{single}(a_2, b)$, then $a_1 = a_2$.

Finsupp.single_left_inj theorem

(h : b ≠ 0) : single a b = single a' b ↔ a = a'

Full source

theorem single_left_inj (h : b ≠ 0) : singlesingle a b = single a' b ↔ a = a' :=
  (single_left_injective h).eq_iff

Injectivity of Single-Point Finitely Supported Function in First Argument for Nonzero Value: $\text{single}(a, b) = \text{single}(a', b) \leftrightarrow a = a'$ when $b \neq 0$

Informal description

For any nonzero element $b$ in a type $M$ with a zero element, the finitely supported functions $\text{single}(a, b)$ and $\text{single}(a', b)$ are equal if and only if $a = a'$.

Finsupp.apply_surjective theorem

(a : α) : Surjective fun f : α →₀ M ↦ f a

Full source

lemma apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
  RightInverse.surjective fun _ ↦ single_eq_same

Surjectivity of Evaluation on Finitely Supported Functions

Informal description

For any element $a$ in a type $\alpha$, the evaluation map $f \mapsto f(a)$ is surjective on the space of finitely supported functions $\alpha \to₀ M$ (where $M$ has a zero element). That is, for any $m \in M$, there exists a finitely supported function $f : \alpha \to₀ M$ such that $f(a) = m$.

Finsupp.support_single_ne_bot theorem

(i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥

Full source

theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
  simpa only [support_single_ne_zero _ h] using singleton_ne_empty _

Nonempty Support of Nonzero Single Finitely Supported Function

Informal description

For any element $i$ in a type $\alpha$ and any nonzero element $b$ in an additive monoid $M$, the support of the finitely supported function $\text{single}(i, b)$ is nonempty.

Finsupp.support_single_disjoint theorem

{b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} : Disjoint (single i b).support (single j b').support ↔ i ≠ j

Full source

theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
    DisjointDisjoint (single i b).support (single j b').support ↔ i ≠ j := by
  rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]

Disjointness of Supports for Single Finitely Supported Functions with Distinct Points

Informal description

For any elements $i, j$ in a type $\alpha$ and nonzero elements $b, b'$ in an additive monoid $M$, the supports of the finitely supported functions $\text{single}(i, b)$ and $\text{single}(j, b')$ are disjoint if and only if $i \neq j$.

Finsupp.single_eq_zero theorem

: single a b = 0 ↔ b = 0

Full source

@[simp]
theorem single_eq_zero : singlesingle a b = 0 ↔ b = 0 := by
  simp [DFunLike.ext_iff, single_eq_set_indicator]

Zero Condition for Single-Point Finitely Supported Function

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function $\text{single}(a, b)$ is equal to the zero function if and only if $b$ is equal to the zero element of $M$. In mathematical notation: $$\text{single}(a, b) = 0 \leftrightarrow b = 0$$

Finsupp.single_ne_zero theorem

: single a b ≠ 0 ↔ b ≠ 0

Full source

theorem single_ne_zero : singlesingle a b ≠ 0single a b ≠ 0 ↔ b ≠ 0 :=
  single_eq_zero.not

Nonzero Condition for Single-Point Finitely Supported Function

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the finitely supported function $\text{single}(a, b)$ is nonzero if and only if $b$ is nonzero. In mathematical notation: $$\text{single}(a, b) \neq 0 \leftrightarrow b \neq 0$$

Finsupp.single_swap theorem

(a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁

Full source

theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ := by
  classical simp only [single_apply, eq_comm]

Symmetry of Single-Point Finitely Supported Function Evaluation

Informal description

For any elements $a_1, a_2 \in \alpha$ and $b \in M$, the finitely supported function `single a₁ b` evaluated at $a_2$ equals the finitely supported function `single a₂ b` evaluated at $a_1$. In mathematical notation: $$(\text{single } a_1 \, b)(a_2) = (\text{single } a_2 \, b)(a_1)$$

Finsupp.instNontrivial instance

[Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M)

Full source

instance instNontrivial [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M) := by
  inhabit α
  rcases exists_ne (0 : M) with ⟨x, hx⟩
  exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)

Nontriviality of Finitely Supported Function Space

Informal description

For any nonempty type $\alpha$ and nontrivial type $M$ with a zero element, the type of finitely supported functions $\alpha \to_{\text{f}} M$ is also nontrivial.

Finsupp.unique_single theorem

[Unique α] (x : α →₀ M) : x = single default (x default)

Full source

theorem unique_single [Unique α] (x : α →₀ M) : x = single default (x default) :=
  ext <| Unique.forall_iff.2 single_eq_same.symm

Characterization of Finitely Supported Functions on a Unique Domain

Informal description

Let $\alpha$ be a type with a unique element (i.e., there exists a unique $a \in \alpha$), and let $M$ be a type with a zero element. For any finitely supported function $x \colon \alpha \to₀ M$, $x$ is equal to the single-point finitely supported function that takes the value $x(\text{default})$ at the unique element of $\alpha$ and zero elsewhere. In mathematical notation: $$x = \text{single}(\text{default}, x(\text{default}))$$

Finsupp.unique_single_eq_iff theorem

[Unique α] {b' : M} : single a b = single a' b' ↔ b = b'

Full source

@[simp]
theorem unique_single_eq_iff [Unique α] {b' : M} : singlesingle a b = single a' b' ↔ b = b' := by
  rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]

Equality of Single-Point Finitely Supported Functions on Unique Domain

Informal description

Let $\alpha$ be a type with a unique element (i.e., there exists exactly one element in $\alpha$), and let $M$ be a type with a zero element. For any elements $b, b' \in M$, the finitely supported functions $\text{single}(a, b)$ and $\text{single}(a', b')$ are equal if and only if $b = b'$.

Finsupp.apply_single' theorem

[Zero N] [Zero P] (e : N → P) (he : e 0 = 0) (a : α) (n : N) (b : α) : e ((single a n) b) = single a (e n) b

Full source

lemma apply_single' [Zero N] [Zero P] (e : N → P) (he : e 0 = 0) (a : α) (n : N) (b : α) :
    e ((single a n) b) = single a (e n) b := by
  classical
  simp only [single_apply]
  split_ifs
  · rfl
  · exact he

Compatibility of Function Application with Single-Point Finitely Supported Functions

Informal description

Let $N$ and $P$ be types with zero elements, and let $e \colon N \to P$ be a function such that $e(0) = 0$. For any elements $a, b \in \alpha$ and $n \in N$, the function $e$ applied to the value of the finitely supported function $\text{single}_a n$ at $b$ is equal to the value of the finitely supported function $\text{single}_a (e(n))$ at $b$. In mathematical notation: $$e\big((\text{single}_a n)(b)\big) = (\text{single}_a (e(n)))(b)$$

Finsupp.apply_single theorem

 [Zero N] [Zero P] {F : Type*} [FunLike F N P] [ZeroHomClass F N P] (e : F) (a : α) (n : N) (b : α) :
  e ((single a n) b) = single a (e n) b

Full source

lemma apply_single [Zero N] [Zero P] {F : Type*} [FunLike F N P] [ZeroHomClass F N P]
    (e : F) (a : α) (n : N) (b : α) :
    e ((single a n) b) = single a (e n) b :=
  apply_single' e (map_zero e) a n b

Zero-Preserving Function Application Commutes with Single-Point Finitely Supported Functions

Informal description

Let $N$ and $P$ be types with zero elements, and let $F$ be a type of functions from $N$ to $P$ that preserves zero (i.e., $F$ has a `ZeroHomClass` instance). For any function $e \in F$, any elements $a, b \in \alpha$, and any $n \in N$, the application of $e$ to the value of the finitely supported function $\text{single}_a n$ at $b$ is equal to the value of the finitely supported function $\text{single}_a (e(n))$ at $b$. In mathematical notation: $$e\big((\text{single}_a n)(b)\big) = (\text{single}_a (e(n)))(b)$$

Finsupp.support_eq_singleton theorem

{f : α →₀ M} {a : α} : f.support = { a } ↔ f a ≠ 0 ∧ f = single a (f a)

Full source

theorem support_eq_singleton {f : α →₀ M} {a : α} :
    f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a) :=
  ⟨fun h =>
    ⟨mem_support_iff.1 <| h.symm ▸ Finset.mem_singleton_self a,
      eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩,
    fun h => h.2.symm ▸ support_single_ne_zero _ h.1⟩

Characterization of Finitely Supported Functions with Singleton Support as Single Functions

Informal description

For a finitely supported function $f \colon \alpha \to M$ and an element $a \in \alpha$, the support of $f$ is the singleton set $\{a\}$ if and only if $f(a) \neq 0$ and $f$ is equal to the function that takes the value $f(a)$ at $a$ and zero everywhere else (i.e., $f = \text{single}_a (f(a))$).

Finsupp.support_eq_singleton' theorem

{f : α →₀ M} {a : α} : f.support = { a } ↔ ∃ b ≠ 0, f = single a b

Full source

theorem support_eq_singleton' {f : α →₀ M} {a : α} :
    f.support = {a} ↔ ∃ b ≠ 0, f = single a b :=
  ⟨fun h =>
    let h := support_eq_singleton.1 h
    ⟨_, h.1, h.2⟩,
    fun ⟨_b, hb, hf⟩ => hf.symm ▸ support_single_ne_zero _ hb⟩

Characterization of Singleton-Supported Functions via Nonzero Single Value

Informal description

For a finitely supported function $f \colon \alpha \to M$ and an element $a \in \alpha$, the support of $f$ is the singleton set $\{a\}$ if and only if there exists a nonzero element $b \in M$ such that $f$ is equal to the function that takes the value $b$ at $a$ and zero everywhere else (i.e., $f = \text{single}_a b$).

Finsupp.card_support_eq_one theorem

{f : α →₀ M} : #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)

Full source

theorem card_support_eq_one {f : α →₀ M} :
    #f.support#f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a) := by
  simp only [card_eq_one, support_eq_singleton]

Characterization of Finitely Supported Functions with Singleton Support

Informal description

For a finitely supported function $f \colon \alpha \to M$, the cardinality of its support is equal to 1 if and only if there exists an element $a \in \alpha$ such that $f(a) \neq 0$ and $f$ is equal to the function `single a (f a)`, which is zero everywhere except at $a$ where it takes the value $f(a)$.

Finsupp.card_support_eq_one' theorem

{f : α →₀ M} : #f.support = 1 ↔ ∃ a, ∃ b ≠ 0, f = single a b

Full source

theorem card_support_eq_one' {f : α →₀ M} :
    #f.support#f.support = 1 ↔ ∃ a, ∃ b ≠ 0, f = single a b := by
  simp only [card_eq_one, support_eq_singleton']

Characterization of Finitely Supported Functions with Singleton Support via Nonzero Value

Informal description

For a finitely supported function $f \colon \alpha \to M$, the cardinality of its support is equal to 1 if and only if there exists an element $a \in \alpha$ and a nonzero element $b \in M$ such that $f$ is equal to the function that takes the value $b$ at $a$ and zero everywhere else.

Finsupp.support_subset_singleton theorem

{f : α →₀ M} {a : α} : f.support ⊆ { a } ↔ f = single a (f a)

Full source

theorem support_subset_singleton {f : α →₀ M} {a : α} : f.support ⊆ {a}f.support ⊆ {a} ↔ f = single a (f a) :=
  ⟨fun h => eq_single_iff.mpr ⟨h, rfl⟩, fun h => (eq_single_iff.mp h).left⟩

Support of Finitely Supported Function is Subset of Singleton if and Only if It is a Single Nonzero Value Function

Informal description

For a finitely supported function $f \colon \alpha \to M$ and an element $a \in \alpha$, the support of $f$ is a subset of the singleton $\{a\}$ if and only if $f$ is equal to the function that takes the value $f(a)$ at $a$ and zero elsewhere.

Finsupp.support_subset_singleton' theorem

{f : α →₀ M} {a : α} : f.support ⊆ { a } ↔ ∃ b, f = single a b

Full source

theorem support_subset_singleton' {f : α →₀ M} {a : α} : f.support ⊆ {a}f.support ⊆ {a} ↔ ∃ b, f = single a b :=
  ⟨fun h => ⟨f a, support_subset_singleton.mp h⟩, fun ⟨b, hb⟩ => by
    rw [hb, support_subset_singleton, single_eq_same]⟩

Support Subset Singleton Characterization for Finitely Supported Functions

Informal description

For a finitely supported function $f \colon \alpha \to M$ and an element $a \in \alpha$, the support of $f$ is a subset of the singleton $\{a\}$ if and only if there exists an element $b \in M$ such that $f$ is equal to the function that takes the value $b$ at $a$ and zero elsewhere.

Finsupp.card_support_le_one theorem

[Nonempty α] {f : α →₀ M} : #f.support ≤ 1 ↔ ∃ a, f = single a (f a)

Full source

theorem card_support_le_one [Nonempty α] {f : α →₀ M} :
    #f.support#f.support ≤ 1 ↔ ∃ a, f = single a (f a) := by
  simp only [card_le_one_iff_subset_singleton, support_subset_singleton]

Support of Finitely Supported Function Has Cardinality at Most One if and Only if It is a Single Nonzero Value Function

Informal description

For a nonempty type $\alpha$ and a finitely supported function $f \colon \alpha \to₀ M$, the support of $f$ has cardinality at most 1 if and only if there exists an element $a \in \alpha$ such that $f$ is equal to the finitely supported function that takes the value $f(a)$ at $a$ and zero elsewhere.

Finsupp.card_support_le_one' theorem

[Nonempty α] {f : α →₀ M} : #f.support ≤ 1 ↔ ∃ a b, f = single a b

Full source

theorem card_support_le_one' [Nonempty α] {f : α →₀ M} :
    #f.support#f.support ≤ 1 ↔ ∃ a b, f = single a b := by
  simp only [card_le_one_iff_subset_singleton, support_subset_singleton']

Finitely Supported Function Has Singleton Support if and Only if It is a Single Nonzero Value Function

Informal description

For a nonempty type $\alpha$ and a finitely supported function $f \colon \alpha \to M$, the support of $f$ has cardinality at most 1 if and only if there exist elements $a \in \alpha$ and $b \in M$ such that $f$ is equal to the function that takes value $b$ at $a$ and zero elsewhere.

Finsupp.equivFunOnFinite_single theorem

[DecidableEq α] [Finite α] (x : α) (m : M) : Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m

Full source

@[simp]
theorem equivFunOnFinite_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m := by
  ext
  simp [Finsupp.single_eq_pi_single, equivFunOnFinite]

Equivalence of Single-Point Finitely Supported Function and Pointwise Single Function on Finite Type

Informal description

Let $\alpha$ be a finite type with decidable equality, and let $M$ be a type with a zero element. For any $x \in \alpha$ and $m \in M$, the equivalence `equivFunOnFinite` maps the finitely supported function `single x m` to the pointwise single function `Pi.single x m`. In other words, under the equivalence between finitely supported functions and all functions on $\alpha$, the function that is $m$ at $x$ and zero elsewhere corresponds to the pointwise function that is $m$ at $x$ and zero elsewhere.

Finsupp.equivFunOnFinite_symm_single theorem

[DecidableEq α] [Finite α] (x : α) (m : M) : Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m

Full source

@[simp]
theorem equivFunOnFinite_symm_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m := by
  rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]

Inverse Equivalence Maps Pointwise Single Function to Finitely Supported Single Function

Informal description

Let $\alpha$ be a finite type with decidable equality and $M$ be a type with a zero element. For any $x \in \alpha$ and $m \in M$, the inverse of the equivalence `equivFunOnFinite` maps the pointwise single function `Pi.single x m` to the finitely supported function `single x m`. In other words, under the inverse of the equivalence between finitely supported functions and all functions on $\alpha$, the pointwise function that is $m$ at $x$ and zero elsewhere corresponds to the finitely supported function that is $m$ at $x$ and zero elsewhere.

Finsupp.update definition

(f : α →₀ M) (a : α) (b : M) : α →₀ M

Full source

/-- Replace the value of a `α →₀ M` at a given point `a : α` by a given value `b : M`.
If `b = 0`, this amounts to removing `a` from the `Finsupp.support`.
Otherwise, if `a` was not in the `Finsupp.support`, it is added to it.

This is the finitely-supported version of `Function.update`. -/
def update (f : α →₀ M) (a : α) (b : M) : α →₀ M where
  support := by
    haveI := Classical.decEq α; haveI := Classical.decEq M
    exact if b = 0 then f.support.erase a else insert a f.support
  toFun :=
    haveI := Classical.decEq α
    Function.update f a b
  mem_support_toFun i := by
    classical
    rw [Function.update]
    simp only [eq_rec_constant, dite_eq_ite, ne_eq]
    split_ifs with hb ha ha <;>
      try simp only [*, not_false_iff, iff_true, not_true, iff_false]
    · rw [Finset.mem_erase]
      simp
    · rw [Finset.mem_erase]
      simp [ha]
    · rw [Finset.mem_insert]
      simp [ha]
    · rw [Finset.mem_insert]
      simp [ha]

Update of a finitely supported function at a point

Informal description

Given a finitely supported function $f : \alpha \to M$ (where $M$ has a zero element), a point $a \in \alpha$, and a value $b \in M$, the function `Finsupp.update f a b` returns a new finitely supported function that is equal to $f$ everywhere except at $a$, where it takes the value $b$. If $b = 0$, this operation effectively removes $a$ from the support of $f$ (if it was present). If $b \neq 0$ and $a$ was not in the support of $f$, it is added to the support.

Finsupp.coe_update theorem

[DecidableEq α] : (f.update a b : α → M) = Function.update f a b

Full source

@[simp, norm_cast]
theorem coe_update [DecidableEq α] : (f.update a b : α → M) = Function.update f a b := by
  delta update Function.update
  ext
  dsimp
  split_ifs <;> simp

Coefficient-wise Update of Finitely Supported Function

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element), any point $a \in \alpha$, and any value $b \in M$, the underlying function of the updated finitely supported function $f.\text{update}\,a\,b$ is equal to the pointwise update of $f$ at $a$ with value $b$, i.e., $(f.\text{update}\,a\,b)(x) = \begin{cases} b & \text{if } x = a, \\ f(x) & \text{otherwise.} \end{cases}$

Finsupp.update_self theorem

: f.update a (f a) = f

Full source

@[simp]
theorem update_self : f.update a (f a) = f := by
  classical
    ext
    simp

Update with Same Value Preserves Function

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element) and any point $a \in \alpha$, updating $f$ at $a$ with its current value $f(a)$ leaves $f$ unchanged, i.e., $f.\text{update}(a, f(a)) = f$.

Finsupp.zero_update theorem

: update 0 a b = single a b

Full source

@[simp]
theorem zero_update : update 0 a b = single a b := by
  classical
    ext
    rw [single_eq_update, coe_update, coe_zero]

Update of Zero Function Yields Single-Point Function

Informal description

For any type $\alpha$ with decidable equality and any type $M$ with a zero element, updating the zero function in $\alpha \to_{\text{f}} M$ at a point $a \in \alpha$ with a value $b \in M$ yields the finitely supported function that is equal to $b$ at $a$ and zero elsewhere. In other words, $\text{update}\,0\,a\,b = \text{single}\,a\,b$.

Finsupp.support_update theorem

[DecidableEq α] [DecidableEq M] : support (f.update a b) = if b = 0 then f.support.erase a else insert a f.support

Full source

theorem support_update [DecidableEq α] [DecidableEq M] :
    support (f.update a b) = if b = 0 then f.support.erase a else insert a f.support := by
  classical
  dsimp only [update]
  congr!

Support of Updated Finitely Supported Function

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element and $\alpha$ and $M$ have decidable equality), a point $a \in \alpha$, and a value $b \in M$, the support of the updated function $f.\text{update}(a, b)$ is given by: \[ \text{support}(f.\text{update}(a, b)) = \begin{cases} \text{support}(f) \setminus \{a\} & \text{if } b = 0 \\ \{a\} \cup \text{support}(f) & \text{otherwise} \end{cases} \]

Finsupp.support_update_zero theorem

[DecidableEq α] : support (f.update a 0) = f.support.erase a

Full source

@[simp]
theorem support_update_zero [DecidableEq α] : support (f.update a 0) = f.support.erase a := by
  classical
  simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
  congr!

Support of Finitely Supported Function After Zero Update

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element) and any point $a \in \alpha$, the support of the updated function $f.\text{update}(a, 0)$ is equal to the support of $f$ with the point $a$ removed, i.e., $\text{support}(f.\text{update}(a, 0)) = \text{support}(f) \setminus \{a\}$.

Finsupp.support_update_ne_zero theorem

[DecidableEq α] (h : b ≠ 0) : support (f.update a b) = insert a f.support

Full source

theorem support_update_ne_zero [DecidableEq α] (h : b ≠ 0) :
    support (f.update a b) = insert a f.support := by
  classical
  simp only [update, h, ite_false, mem_support_iff, ne_eq]
  congr!

Support of Finitely Supported Function Update with Nonzero Value

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element), a point $a \in \alpha$, and a nonzero value $b \in M$ (i.e., $b \neq 0$), the support of the updated function $f.update(a, b)$ is equal to the union of $\{a\}$ with the support of $f$, i.e., $\text{support}(f.update(a, b)) = \{a\} \cup \text{support}(f)$.

Finsupp.support_update_subset theorem

[DecidableEq α] : support (f.update a b) ⊆ insert a f.support

Full source

theorem support_update_subset [DecidableEq α] :
    supportsupport (f.update a b) ⊆ insert a f.support := by
  classical
  rw [support_update]
  split_ifs
  · exact (erase_subset _ _).trans (subset_insert _ _)
  · rfl

Support of Updated Finitely Supported Function is Subset of Insertion

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element and $\alpha$ has decidable equality), a point $a \in \alpha$, and a value $b \in M$, the support of the updated function $f.\text{update}(a, b)$ is a subset of the union of $\{a\}$ with the support of $f$, i.e., $\text{support}(f.\text{update}(a, b)) \subseteq \{a\} \cup \text{support}(f)$.

Finsupp.update_comm theorem

 (f : α →₀ M) {a₁ a₂ : α} (h : a₁ ≠ a₂) (m₁ m₂ : M) : update (update f a₁ m₁) a₂ m₂ = update (update f a₂ m₂) a₁ m₁

Full source

theorem update_comm (f : α →₀ M) {a₁ a₂ : α} (h : a₁ ≠ a₂) (m₁ m₂ : M) :
    update (update f a₁ m₁) a₂ m₂ = update (update f a₂ m₂) a₁ m₁ :=
  letI := Classical.decEq α
  DFunLike.coe_injective <| Function.update_comm h _ _ _

Commutativity of Updates at Distinct Points for Finitely Supported Functions

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any two distinct points $a_1, a_2 \in \alpha$ (i.e., $a_1 \neq a_2$), updating $f$ at $a_1$ with value $m_1$ and then at $a_2$ with value $m_2$ is equivalent to first updating at $a_2$ with $m_2$ and then at $a_1$ with $m_1$. That is, $$\text{update}(\text{update}(f, a_1, m_1), a_2, m_2) = \text{update}(\text{update}(f, a_2, m_2), a_1, m_1).$$

Finsupp.update_idem theorem

(f : α →₀ M) (a : α) (b c : M) : update (update f a b) a c = update f a c

Full source

@[simp] theorem update_idem (f : α →₀ M) (a : α) (b c : M) :
    update (update f a b) a c = update f a c :=
  letI := Classical.decEq α
  DFunLike.coe_injective <| Function.update_idem _ _ _

Idempotence of Function Update at a Point

Informal description

For any finitely supported function $f \colon \alpha \to M$, any point $a \in \alpha$, and any values $b, c \in M$, updating $f$ at $a$ first with $b$ and then with $c$ is equivalent to updating $f$ at $a$ directly with $c$. That is, $\text{update}(\text{update}(f, a, b), a, c) = \text{update}(f, a, c)$.

Finsupp.erase definition

(a : α) (f : α →₀ M) : α →₀ M

Full source

/--
`erase a f` is the finitely supported function equal to `f` except at `a` where it is equal to `0`.
If `a` is not in the support of `f` then `erase a f = f`.
-/
def erase (a : α) (f : α →₀ M) : α →₀ M where
  support :=
    haveI := Classical.decEq α
    f.support.erase a
  toFun a' :=
    haveI := Classical.decEq α
    if a' = a then 0 else f a'
  mem_support_toFun a' := by
    classical
    rw [mem_erase, mem_support_iff]; dsimp
    split_ifs with h
    · exact ⟨fun H _ => H.1 h, fun H => (H rfl).elim⟩
    · exact and_iff_right h

Erase a point from a finitely supported function

Informal description

The function `erase a f` takes a finitely supported function `f : α →₀ M` and returns a new finitely supported function that is equal to `f` everywhere except at the point `a`, where it is set to `0`. If `a` is not in the support of `f`, then `erase a f` is equal to `f`.

Finsupp.support_erase theorem

[DecidableEq α] {a : α} {f : α →₀ M} : (f.erase a).support = f.support.erase a

Full source

@[simp]
theorem support_erase [DecidableEq α] {a : α} {f : α →₀ M} :
    (f.erase a).support = f.support.erase a := by
  classical
  dsimp only [erase]
  congr!

Support of Erased Function Equals Support Minus Point

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any point $a \in \alpha$, the support of the function $f \setminus a$ (obtained by erasing $a$ from $f$) is equal to the set obtained by removing $a$ from the support of $f$. That is, $\text{support}(f \setminus a) = \text{support}(f) \setminus \{a\}$.

Finsupp.erase_same theorem

{a : α} {f : α →₀ M} : (f.erase a) a = 0

Full source

@[simp]
theorem erase_same {a : α} {f : α →₀ M} : (f.erase a) a = 0 := by
  classical simp only [erase, coe_mk, ite_true]

Erased Point Evaluates to Zero

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any point $a \in \alpha$, the function obtained by erasing $a$ from $f$ satisfies $(f \setminus a)(a) = 0$.

Finsupp.erase_ne theorem

{a a' : α} {f : α →₀ M} (h : a' ≠ a) : (f.erase a) a' = f a'

Full source

@[simp]
theorem erase_ne {a a' : α} {f : α →₀ M} (h : a' ≠ a) : (f.erase a) a' = f a' := by
  classical simp only [erase, coe_mk, h, ite_false]

Evaluation of Erased Function at Distinct Points: $(f \setminus a)(a') = f(a')$ for $a' \neq a$

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any distinct points $a, a' \in \alpha$, the function obtained by erasing $a$ from $f$ satisfies $(f \setminus a)(a') = f(a')$.

Finsupp.erase_apply theorem

[DecidableEq α] {a a' : α} {f : α →₀ M} : f.erase a a' = if a' = a then 0 else f a'

Full source

theorem erase_apply [DecidableEq α] {a a' : α} {f : α →₀ M} :
    f.erase a a' = if a' = a then 0 else f a' := by
  rw [erase, coe_mk]
  simp only [ite_eq_ite]

Evaluation of Erased Finitely Supported Function: $(f \setminus a)(a') = \begin{cases} 0 & \text{if } a' = a \\ f(a') & \text{otherwise} \end{cases}$

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any points $a, a' \in \alpha$, the function obtained by erasing $a$ from $f$ satisfies $(f \setminus a)(a') = 0$ if $a' = a$, and $(f \setminus a)(a') = f(a')$ otherwise.

Finsupp.erase_single theorem

{a : α} {b : M} : erase a (single a b) = 0

Full source

@[simp]
theorem erase_single {a : α} {b : M} : erase a (single a b) = 0 := by
  ext s; by_cases hs : s = a
  · rw [hs, erase_same, coe_zero, Pi.zero_apply]
  · rw [erase_ne hs]
    exact single_eq_of_ne (Ne.symm hs)

Erasing Single-Point Function Yields Zero Function

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the function obtained by erasing $a$ from the finitely supported function $\text{single}(a, b)$ is the zero function, i.e., $\text{erase}(a, \text{single}(a, b)) = 0$.

Finsupp.erase_single_ne theorem

{a a' : α} {b : M} (h : a ≠ a') : erase a (single a' b) = single a' b

Full source

theorem erase_single_ne {a a' : α} {b : M} (h : a ≠ a') : erase a (single a' b) = single a' b := by
  ext s; by_cases hs : s = a
  · rw [hs, erase_same, single_eq_of_ne h.symm]
  · rw [erase_ne hs]

Erasing a Point from a Single-Point Function Leaves It Unchanged When Points Are Distinct

Informal description

For any distinct elements $a$ and $a'$ in a type $\alpha$ and any element $b$ in a type $M$ with a zero element, the operation of erasing $a$ from the finitely supported function $\text{single}(a', b)$ leaves the function unchanged, i.e., $\text{erase}(a, \text{single}(a', b)) = \text{single}(a', b)$.

Finsupp.erase_of_not_mem_support theorem

{f : α →₀ M} {a} (haf : a ∉ f.support) : erase a f = f

Full source

@[simp]
theorem erase_of_not_mem_support {f : α →₀ M} {a} (haf : a ∉ f.support) : erase a f = f := by
  ext b; by_cases hab : b = a
  · rwa [hab, erase_same, eq_comm, ← not_mem_support_iff]
  · rw [erase_ne hab]

Erasing a Point Outside Support Leaves Function Unchanged

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} M$ and any point $a \in \alpha$ not in the support of $f$, the function obtained by erasing $a$ from $f$ is equal to $f$ itself, i.e., $f \setminus a = f$.

Finsupp.erase_zero theorem

(a : α) : erase a (0 : α →₀ M) = 0

Full source

theorem erase_zero (a : α) : erase a (0 : α →₀ M) = 0 := by
  simp

Erasing from Zero Function Yields Zero

Informal description

For any element $a$ in a type $\alpha$, erasing $a$ from the zero function (the function that maps every element of $\alpha$ to $0_M$) yields the zero function again, i.e., $\operatorname{erase}_a(0) = 0$.

Finsupp.erase_eq_update_zero theorem

(f : α →₀ M) (a : α) : f.erase a = update f a 0

Full source

theorem erase_eq_update_zero (f : α →₀ M) (a : α) : f.erase a = update f a 0 :=
  letI := Classical.decEq α
  ext fun _ => (Function.update_apply _ _ _ _).symm

Erase Equals Update with Zero

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any point $a \in \alpha$, the function obtained by erasing $a$ from $f$ (i.e., setting $f(a) = 0$) is equal to updating $f$ at $a$ with the value $0$. In other words, $\operatorname{erase}_a(f) = \operatorname{update}(f, a, 0)$.

Finsupp.erase_update_of_ne theorem

(f : α →₀ M) {a a' : α} (ha : a ≠ a') (b : M) : erase a (update f a' b) = update (erase a f) a' b

Full source

theorem erase_update_of_ne (f : α →₀ M) {a a' : α} (ha : a ≠ a') (b : M) :
    erase a (update f a' b) = update (erase a f) a' b := by
  rw [erase_eq_update_zero, erase_eq_update_zero, update_comm _ ha]

Commutation of Erase and Update at Distinct Points for Finitely Supported Functions

Informal description

For any finitely supported function $f \colon \alpha \to M$ and distinct points $a, a' \in \alpha$ (i.e., $a \neq a'$), erasing $a$ from the function obtained by updating $f$ at $a'$ with value $b$ is equal to updating the function obtained by erasing $a$ from $f$ at $a'$ with value $b$. That is, $$\operatorname{erase}_a(\operatorname{update}(f, a', b)) = \operatorname{update}(\operatorname{erase}_a(f), a', b).$$

Finsupp.erase_idem theorem

(f : α →₀ M) (a : α) : erase a (erase a f) = erase a f

Full source

theorem erase_idem (f : α →₀ M) (a : α) :
    erase a (erase a f) = erase a f := by
  rw [erase_eq_update_zero, erase_eq_update_zero, update_idem]

Idempotence of Erasure in Finitely Supported Functions

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any point $a \in \alpha$, erasing $a$ twice from $f$ is equivalent to erasing it once. That is, $\operatorname{erase}_a(\operatorname{erase}_a(f)) = \operatorname{erase}_a(f)$.

Finsupp.update_erase_eq_update theorem

(f : α →₀ M) (a : α) (b : M) : update (erase a f) a b = update f a b

Full source

@[simp] theorem update_erase_eq_update (f : α →₀ M) (a : α) (b : M) :
    update (erase a f) a b = update f a b := by
  rw [erase_eq_update_zero, update_idem]

Update After Erase Equals Direct Update

Informal description

For any finitely supported function $f \colon \alpha \to M$, any point $a \in \alpha$, and any value $b \in M$, updating the function obtained by erasing $a$ from $f$ (i.e., setting $f(a) = 0$) at $a$ with value $b$ is equal to updating $f$ directly at $a$ with value $b$. In other words, $\text{update}(\text{erase}_a(f), a, b) = \text{update}(f, a, b)$.

Finsupp.erase_update_eq_erase theorem

(f : α →₀ M) (a : α) (b : M) : erase a (update f a b) = erase a f

Full source

@[simp] theorem erase_update_eq_erase (f : α →₀ M) (a : α) (b : M) :
    erase a (update f a b) = erase a f := by
  rw [erase_eq_update_zero, erase_eq_update_zero, update_idem]

Erase Commutes with Update at Same Point

Informal description

For any finitely supported function $f \colon \alpha \to M$, any point $a \in \alpha$, and any value $b \in M$, erasing $a$ from the function obtained by updating $f$ at $a$ with $b$ is equal to erasing $a$ from $f$ itself. That is, $\operatorname{erase}_a(\operatorname{update}(f, a, b)) = \operatorname{erase}_a(f)$.

Finsupp.mapRange_single theorem

{f : M → N} {hf : f 0 = 0} {a : α} {b : M} : mapRange f hf (single a b) = single a (f b)

Full source

@[simp]
theorem mapRange_single {f : M → N} {hf : f 0 = 0} {a : α} {b : M} :
    mapRange f hf (single a b) = single a (f b) :=
  ext fun a' => by
    classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'

Mapping Range Preserves Single-Point Function: $\text{mapRange}\, f\, (\text{single}\, a\, b) = \text{single}\, a\, (f(b))$

Informal description

Let $f \colon M \to N$ be a function such that $f(0) = 0$. For any element $a \in \alpha$ and any value $b \in M$, applying the function `mapRange` to the single-point finitely supported function `single a b` yields the single-point finitely supported function `single a (f b)`. In mathematical notation: $$\text{mapRange}\, f\, hf\, (\text{single}\, a\, b) = \text{single}\, a\, (f(b)).$$

Finsupp.single_of_embDomain_single theorem

 (l : α →₀ M) (f : α ↪ β) (a : β) (b : M) (hb : b ≠ 0) (h : l.embDomain f = single a b) : ∃ x, l = single x b ∧ f x = a

Full source

theorem single_of_embDomain_single (l : α →₀ M) (f : α ↪ β) (a : β) (b : M) (hb : b ≠ 0)
    (h : l.embDomain f = single a b) : ∃ x, l = single x b ∧ f x = a := by
  classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single_ne_zero _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply f l, h]
      by_cases h_cases : c = d
      · simp only [Eq.symm h_cases, hc₂, single_eq_same]
      · rw [single_apply, single_apply, if_neg, if_neg h_cases]
        by_contra hfd
        exact h_cases (f.injective (hc₂.trans hfd))
    · exact hc₂

Characterization of Single-Point Functions via Embedding

Informal description

Let $l \colon \alpha \to₀ M$ be a finitely supported function, $f \colon \alpha \hookrightarrow \beta$ an embedding, $a \in \beta$, and $b \in M$ with $b \neq 0$. If the embedded function $\text{embDomain}\, f\, l$ is equal to the single-point function $\text{single}(a, b)$, then there exists an element $x \in \alpha$ such that $l = \text{single}(x, b)$ and $f(x) = a$.

Finsupp.embDomain_single theorem

(f : α ↪ β) (a : α) (m : M) : embDomain f (single a m) = single (f a) m

Full source

@[simp]
theorem embDomain_single (f : α ↪ β) (a : α) (m : M) :
    embDomain f (single a m) = single (f a) m := by
  classical
    ext b
    by_cases h : b ∈ Set.range f
    · rcases h with ⟨a', rfl⟩
      simp [single_apply]
    · simp only [embDomain_notin_range, h, single_apply, not_false_iff]
      rw [if_neg]
      rintro rfl
      simp at h

Embedding Preserves Single-Point Finitely Supported Function

Informal description

Given an embedding $f \colon \alpha \hookrightarrow \beta$, an element $a \in \alpha$, and a value $m \in M$, the embedded finitely supported function $\text{embDomain}\, f\, (\text{single}\, a\, m)$ is equal to the finitely supported function $\text{single}\, (f(a))\, m$ on $\beta$. In mathematical notation: $$\text{embDomain}\, f\, (\text{single}\, a\, m) = \text{single}\, (f(a))\, m.$$

Finsupp.zipWith_single_single theorem

 (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) : zipWith f hf (single a m) (single a n) = single a (f m n)

Full source

@[simp]
theorem zipWith_single_single (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) :
    zipWith f hf (single a m) (single a n) = single a (f m n) := by
  ext a'
  rw [zipWith_apply]
  obtain rfl | ha' := eq_or_ne a a'
  · rw [single_eq_same, single_eq_same, single_eq_same]
  · rw [single_eq_of_ne ha', single_eq_of_ne ha', single_eq_of_ne ha', hf]

Pointwise Combination of Single-Point Finitely Supported Functions

Informal description

Let $f \colon M \to N \to P$ be a function such that $f(0, 0) = 0$. For any element $a \in \alpha$ and any elements $m \in M$, $n \in N$, the pointwise combination of the finitely supported functions $\operatorname{single}(a, m)$ and $\operatorname{single}(a, n)$ satisfies \[ \operatorname{zipWith}(f, hf, \operatorname{single}(a, m), \operatorname{single}(a, n)) = \operatorname{single}(a, f(m, n)). \]

Finsupp.single_add theorem

(a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂

Full source

@[simp]
theorem single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  (zipWith_single_single _ _ _ _ _).symm

Additivity of Single-Point Finitely Supported Functions

Informal description

For any element $a \in \alpha$ and any elements $b_1, b_2 \in M$, the finitely supported function with a single nonzero value at $a$ satisfies: \[ \operatorname{single}(a, b_1 + b_2) = \operatorname{single}(a, b_1) + \operatorname{single}(a, b_2). \]

Finsupp.support_single_add theorem

 {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : support (single a b + f) = cons a f.support ha

Full source

theorem support_single_add {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
    support (single a b + f) = cons a f.support ha := by
  classical
  have H := support_single_ne_zero a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]

Support of Sum of Single-Point Function and Function with Disjoint Support

Informal description

Let $\alpha$ be a type with decidable equality and $M$ be a type with a zero element. For any element $a \in \alpha$, any nonzero element $b \in M$, and any finitely supported function $f \colon \alpha \to₀ M$ such that $a$ is not in the support of $f$, the support of the sum $\operatorname{single}(a, b) + f$ is equal to the set obtained by inserting $a$ into the support of $f$, i.e., $\operatorname{supp}(\operatorname{single}(a, b) + f) = \{a\} \cup \operatorname{supp}(f)$.

Finsupp.support_add_single theorem

 {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : support (f + single a b) = cons a f.support ha

Full source

theorem support_add_single {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
    support (f + single a b) = cons a f.support ha := by
  classical
  have H := support_single_ne_zero a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]

Support of Sum with Single-Point Function When Disjoint

Informal description

Let $\alpha$ be a type with decidable equality and $M$ be a type with a zero element. For any element $a \in \alpha$, any nonzero element $b \in M$, and any finitely supported function $f \colon \alpha \to₀ M$ such that $a$ is not in the support of $f$, the support of the sum $f + \operatorname{single}(a, b)$ is equal to the set obtained by inserting $a$ into the support of $f$, i.e., $\operatorname{supp}(f + \operatorname{single}(a, b)) = \{a\} \cup \operatorname{supp}(f)$.

AddEquiv.finsuppUnique_symm theorem

{M : Type*} [AddZeroClass M] (d : M) : AddEquiv.finsuppUnique.symm d = single () d

Full source

lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
    AddEquiv.finsuppUnique.symm d = single () d := by
  rw [Finsupp.unique_single (AddEquiv.finsuppUnique.symm d), Finsupp.unique_single_eq_iff]
  simp [AddEquiv.finsuppUnique]

Inverse of Additive Equivalence Between Finitely Supported Functions on Singleton Type and Codomain Maps to Single-Point Function

Informal description

Let $M$ be an additive monoid with zero. The inverse of the additive equivalence $\text{finsuppUnique}$ maps any element $d \in M$ to the finitely supported function $\text{single}(\text{()}, d)$, where $\text{()}$ is the unique element of the domain type (a singleton type).

Finsupp.singleAddHom definition

(a : α) : M →+ α →₀ M

Full source

/-- `Finsupp.single` as an `AddMonoidHom`.

See `Finsupp.lsingle` in `Mathlib/LinearAlgebra/Finsupp/Defs.lean` for the stronger version as a
linear map. -/
@[simps]
def singleAddHom (a : α) : M →+ α →₀ M where
  toFun := single a
  map_zero' := single_zero a
  map_add' := single_add a

Additive monoid homomorphism of single-point finitely supported functions

Informal description

For a fixed element $a \in \alpha$, the function $\operatorname{singleAddHom}(a) \colon M \to \alpha \to_{\text{f}} M$ is an additive monoid homomorphism that maps each $b \in M$ to the finitely supported function $\operatorname{single}(a, b)$. Here, $\operatorname{single}(a, b)$ is the function that takes the value $b$ at $a$ and zero elsewhere. The homomorphism satisfies: 1. $\operatorname{singleAddHom}(a)(0) = \operatorname{single}(a, 0)$, and 2. $\operatorname{singleAddHom}(a)(b_1 + b_2) = \operatorname{singleAddHom}(a)(b_1) + \operatorname{singleAddHom}(a)(b_2)$ for all $b_1, b_2 \in M$.

Finsupp.update_eq_single_add_erase theorem

(f : α →₀ M) (a : α) (b : M) : f.update a b = single a b + f.erase a

Full source

theorem update_eq_single_add_erase (f : α →₀ M) (a : α) (b : M) :
    f.update a b = single a b + f.erase a := by
  classical
    ext j
    rcases eq_or_ne a j with (rfl | h)
    · simp
    · simp [Function.update_of_ne h.symm, single_apply, h, erase_ne, h.symm]

Decomposition of Updated Finitely Supported Function: $f.\text{update}\,a\,b = \text{single}(a, b) + f \setminus a$

Informal description

For any finitely supported function $f \colon \alpha \to M$, any point $a \in \alpha$, and any value $b \in M$, the updated function $f.\text{update}\,a\,b$ can be expressed as the sum of the single-point function $\text{single}(a, b)$ and the erased function $f \setminus a$, i.e., $$ f.\text{update}\,a\,b = \text{single}(a, b) + f \setminus a. $$

Finsupp.update_eq_erase_add_single theorem

(f : α →₀ M) (a : α) (b : M) : f.update a b = f.erase a + single a b

Full source

theorem update_eq_erase_add_single (f : α →₀ M) (a : α) (b : M) :
    f.update a b = f.erase a + single a b := by
  classical
    ext j
    rcases eq_or_ne a j with (rfl | h)
    · simp
    · simp [Function.update_of_ne h.symm, single_apply, h, erase_ne, h.symm]

Decomposition of Updated Finitely Supported Function: $f.\text{update}\,a\,b = f \setminus a + \text{single}(a, b)$

Informal description

For any finitely supported function $f \colon \alpha \to M$, any point $a \in \alpha$, and any value $b \in M$, the updated function $f.\text{update}\,a\,b$ can be expressed as the sum of the erased function $f \setminus a$ and the single-point function $\text{single}(a, b)$, i.e., $$ f.\text{update}\,a\,b = f \setminus a + \text{single}(a, b). $$

Finsupp.single_add_erase theorem

(a : α) (f : α →₀ M) : single a (f a) + f.erase a = f

Full source

theorem single_add_erase (a : α) (f : α →₀ M) : single a (f a) + f.erase a = f := by
  rw [← update_eq_single_add_erase, update_self]

Decomposition of Finitely Supported Function: $f = \text{single}(a, f(a)) + f \setminus a$

Informal description

For any finitely supported function $f \colon \alpha \to M$ and any point $a \in \alpha$, the sum of the single-point function $\text{single}(a, f(a))$ and the erased function $f \setminus a$ equals $f$, i.e., $$ \text{single}(a, f(a)) + f \setminus a = f. $$

Finsupp.erase_add_single theorem

(a : α) (f : α →₀ M) : f.erase a + single a (f a) = f

Full source

theorem erase_add_single (a : α) (f : α →₀ M) : f.erase a + single a (f a) = f := by
  rw [← update_eq_erase_add_single, update_self]

Decomposition of Finitely Supported Function via Erasure and Single-Point Addition

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element) and any point $a \in \alpha$, the sum of the erased function $f \setminus a$ and the single-point function $\text{single}(a, f(a))$ equals $f$, i.e., $$ (f \setminus a) + \text{single}(a, f(a)) = f. $$

Finsupp.erase_add theorem

(a : α) (f f' : α →₀ M) : erase a (f + f') = erase a f + erase a f'

Full source

@[simp]
theorem erase_add (a : α) (f f' : α →₀ M) : erase a (f + f') = erase a f + erase a f' := by
  ext s; by_cases hs : s = a
  · rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
  rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

Erasing a Point Commutes with Addition of Finitely Supported Functions

Informal description

For any element $a \in \alpha$ and any two finitely supported functions $f, f' \colon \alpha \to M$, the function obtained by erasing $a$ from the sum of $f$ and $f'$ is equal to the sum of the functions obtained by erasing $a$ from $f$ and $f'$ individually, i.e., $$ (f + f') \setminus a = (f \setminus a) + (f' \setminus a). $$

Finsupp.eraseAddHom definition

(a : α) : (α →₀ M) →+ α →₀ M

Full source

/-- `Finsupp.erase` as an `AddMonoidHom`. -/
@[simps]
def eraseAddHom (a : α) : (α →₀ M) →+ α →₀ M where
  toFun := erase a
  map_zero' := erase_zero a
  map_add' := erase_add a

Erasure as an additive monoid homomorphism

Informal description

For a given element $a \in \alpha$, the function `erase a` is an additive monoid homomorphism from the type of finitely supported functions $\alpha \to_{\text{f}} M$ to itself. It maps a finitely supported function $f$ to the function that coincides with $f$ everywhere except at $a$, where it is set to $0$.

Finsupp.induction theorem

 {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0)
  (single_add : ∀ (a b) (f : α →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f

Full source

@[elab_as_elim]
protected theorem induction {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0)
    (single_add : ∀ (a b) (f : α →₀ M),
      a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f :=
  suffices ∀ (s) (f : α →₀ M), f.support = s → motive f from this _ _ rfl
  fun s =>
  Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
    suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
    classical
      apply single_add
      · rw [support_erase, mem_erase]
        exact fun H => H.1 rfl
      · rw [← mem_support_iff, hf]
        exact mem_cons_self _ _
      · apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

Induction Principle for Finitely Supported Functions

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function. To prove a property $\text{motive}(f)$ holds for all such $f$, it suffices to: 1. Show that $\text{motive}(0)$ holds for the zero function. 2. For any $a \in \alpha$, $b \in M \setminus \{0\}$, and $f \colon \alpha \to_{\text{f}} M$ such that $a \notin \text{support}(f)$, if $\text{motive}(f)$ holds, then $\text{motive}(\text{single}(a, b) + f)$ also holds. Here, $\text{single}(a, b)$ denotes the function that is $b$ at $a$ and zero elsewhere, and $\text{support}(f)$ is the finite set where $f$ is nonzero.

Finsupp.induction₂ theorem

 {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0)
  (add_single : ∀ (a b) (f : α →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f

Full source

@[elab_as_elim]
theorem induction₂ {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0)
    (add_single : ∀ (a b) (f : α →₀ M),
      a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f :=
  suffices ∀ (s) (f : α →₀ M), f.support = s → motive f from this _ _ rfl
  fun s =>
  Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
    suffices motive (f.erase a + single a (f a)) by rwa [erase_add_single] at this
    classical
      apply add_single
      · rw [support_erase, mem_erase]
        exact fun H => H.1 rfl
      · rw [← mem_support_iff, hf]
        exact mem_cons_self _ _
      · apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

Induction Principle for Finitely Supported Functions via Single-Point Addition

Informal description

Let $M$ be a type with a zero element, and let $\alpha$ be any type. Given a finitely supported function $f \colon \alpha \to_{\text{f}} M$ and a predicate $\text{motive}$ on $\alpha \to_{\text{f}} M$, if the following conditions hold: 1. The zero function satisfies $\text{motive}(0)$. 2. For any $a \in \alpha$, $b \in M$ with $b \neq 0$, and $f \colon \alpha \to_{\text{f}} M$ such that $a \notin \text{support}(f)$, if $\text{motive}(f)$ holds, then $\text{motive}(f + \text{single}(a, b))$ also holds, then $\text{motive}(f)$ holds for all $f \colon \alpha \to_{\text{f}} M$.

Finsupp.induction_linear theorem

 {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0) (add : ∀ f g : α →₀ M, motive f → motive g → motive (f + g))
  (single : ∀ a b, motive (single a b)) : motive f

Full source

@[elab_as_elim]
theorem induction_linear {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0)
    (add : ∀ f g : α →₀ M, motive f → motive g → motive (f + g))
    (single : ∀ a b, motive (single a b)) : motive f :=
  induction₂ f zero fun _a _b _f _ _ w => add _ _ w (single _ _)

Linear Induction Principle for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element, and let $\alpha$ be any type. Given a finitely supported function $f \colon \alpha \to_{\text{f}} M$ and a predicate $\text{motive}$ on $\alpha \to_{\text{f}} M$, if the following conditions hold: 1. The zero function satisfies $\text{motive}(0)$. 2. For any two finitely supported functions $f, g \colon \alpha \to_{\text{f}} M$, if $\text{motive}(f)$ and $\text{motive}(g)$ hold, then $\text{motive}(f + g)$ also holds. 3. For any $a \in \alpha$ and $b \in M$, $\text{motive}(\text{single}(a, b))$ holds, where $\text{single}(a, b)$ is the function that is $b$ at $a$ and zero elsewhere, then $\text{motive}(f)$ holds for all $f \colon \alpha \to_{\text{f}} M$.

Finsupp.induction_on_max theorem

 (f : α →₀ M) (h0 : p 0) (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) : p f

Full source

/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.

The theorem `induction_on_max₂` swaps the argument order in the sum. -/
theorem induction_on_max (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) :
    p f := by
  suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl
  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
  · rwa [support_eq_empty.1 h]
  · have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← single_add_erase a f]
    refine ha _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

Induction Principle for Finitely Supported Functions with Maximum Element Condition

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function, and let $p$ be a predicate on such functions. If: 1. $p$ holds for the zero function, and 2. For any $a \in \alpha$, $b \in M$ with $b \neq 0$, and any finitely supported function $f' \colon \alpha \to_{\text{f}} M$, if $p$ holds for $f'$ and for all $c$ in the support of $f'$ we have $c < a$, then $p$ holds for $\text{single}(a, b) + f'$, then $p$ holds for $f$.

Finsupp.induction_on_min theorem

 (f : α →₀ M) (h0 : p 0) (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) : p f

Full source

/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.

The theorem `induction_on_min₂` swaps the argument order in the sum. -/
theorem induction_on_min (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) :
    p f :=
  induction_on_max (α := αᵒᵈ) f h0 ha

Induction Principle for Finitely Supported Functions with Minimal Support Element Condition

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function, and let $p$ be a predicate on such functions. If: 1. $p$ holds for the zero function, and 2. For any $a \in \alpha$, $b \in M$ with $b \neq 0$, and any finitely supported function $f' \colon \alpha \to_{\text{f}} M$, if $p$ holds for $f'$ and for all $c$ in the support of $f'$ we have $a < c$, then $p$ holds for $\text{single}(a, b) + f'$, then $p$ holds for $f$.

Finsupp.induction_on_max₂ theorem

 (f : α →₀ M) (h0 : p 0) (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) : p f

Full source

/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.

The theorem `induction_on_max` swaps the argument order in the sum. -/
theorem induction_on_max₂ (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) :
    p f := by
  suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl
  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
  · rwa [support_eq_empty.1 h]
  · have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← erase_add_single a f]
    refine ha _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

Induction Principle for Finitely Supported Functions by Maximal Support Element

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function, and let $p$ be a predicate on such functions. Suppose: 1. The zero function satisfies $p$. 2. For any $a \in \alpha$, $b \in M$ with $b \neq 0$, and any finitely supported function $f' \colon \alpha \to_{\text{f}} M$, if $p(f')$ holds and for all $c$ in the support of $f'$ we have $c < a$, then $p(f' + \text{single}(a, b))$ holds. Then $p(f)$ holds.

Finsupp.induction_on_min₂ theorem

 (f : α →₀ M) (h0 : p 0) (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) : p f

Full source

/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.

The theorem `induction_on_min` swaps the argument order in the sum. -/
theorem induction_on_min₂ (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) :
    p f :=
  induction_on_max₂ (α := αᵒᵈ) f h0 ha

Induction Principle for Finitely Supported Functions by Minimal Support Element (Version 2)

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function, and let $p$ be a predicate on such functions. Suppose: 1. The zero function satisfies $p$. 2. For any $a \in \alpha$, $b \in M$ with $b \neq 0$, and any finitely supported function $f' \colon \alpha \to_{\text{f}} M$, if $p(f')$ holds and for all $c$ in the support of $f'$ we have $a < c$, then $p(f' + \text{single}(a, b))$ holds. Then $p(f)$ holds.

Finsupp.single_add_single_eq_single_add_single theorem

 [AddCommMonoid M] {k l m n : α} {u v : M} (hu : u ≠ 0) (hv : v ≠ 0) :
  single k u + single l v = single m u + single n v ↔
    (k = m ∧ l = n) ∨ (u = v ∧ k = n ∧ l = m) ∨ (u + v = 0 ∧ k = l ∧ m = n)

Full source

theorem single_add_single_eq_single_add_single [AddCommMonoid M] {k l m n : α} {u v : M}
    (hu : u ≠ 0) (hv : v ≠ 0) :
    singlesingle k u + single l v = single m u + single n v ↔
      (k = m ∧ l = n) ∨ (u = v ∧ k = n ∧ l = m) ∨ (u + v = 0 ∧ k = l ∧ m = n) := by
  classical
    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
    exact Pi.single_add_single_eq_single_add_single hu hv

Equality Condition for Sums of Single-Point Finitely Supported Functions

Informal description

Let $M$ be an additive commutative monoid, and let $k, l, m, n \in \alpha$ and $u, v \in M$ with $u \neq 0$ and $v \neq 0$. Then the equality of finitely supported functions $$ \text{single}(k, u) + \text{single}(l, v) = \text{single}(m, u) + \text{single}(n, v) $$ holds if and only if one of the following conditions is satisfied: 1. $k = m$ and $l = n$, or 2. $u = v$, $k = n$, and $l = m$, or 3. $u + v = 0$, $k = l$, and $m = n$. Here, $\text{single}(a, b)$ denotes the finitely supported function that takes the value $b$ at $a$ and zero elsewhere.

Finsupp.erase_eq_sub_single theorem

[AddGroup G] (f : α →₀ G) (a : α) : f.erase a = f - single a (f a)

Full source

theorem erase_eq_sub_single [AddGroup G] (f : α →₀ G) (a : α) : f.erase a = f - single a (f a) := by
  ext a'
  rcases eq_or_ne a a' with (rfl | h)
  · simp
  · simp [erase_ne h.symm, single_eq_of_ne h]

Erase Equals Subtract Single: $f \setminus a = f - \text{single}(a, f(a))$

Informal description

Let $G$ be an additive group and let $f \colon \alpha \to_{\text{fs}} G$ be a finitely supported function. For any $a \in \alpha$, the function obtained by erasing $a$ from $f$ satisfies $f \setminus a = f - \text{single}(a, f(a))$, where $\text{single}(a, f(a))$ is the finitely supported function that takes the value $f(a)$ at $a$ and zero elsewhere.

Finsupp.update_eq_sub_add_single theorem

[AddGroup G] (f : α →₀ G) (a : α) (b : G) : f.update a b = f - single a (f a) + single a b

Full source

theorem update_eq_sub_add_single [AddGroup G] (f : α →₀ G) (a : α) (b : G) :
    f.update a b = f - single a (f a) + single a b := by
  rw [update_eq_erase_add_single, erase_eq_sub_single]

Decomposition of Updated Finitely Supported Function: $f.\text{update}\,a\,b = f - \text{single}(a, f(a)) + \text{single}(a, b)$

Informal description

Let $G$ be an additive group and let $f \colon \alpha \to_{\text{fs}} G$ be a finitely supported function. For any $a \in \alpha$ and $b \in G$, the updated function $f.\text{update}\,a\,b$ can be expressed as: $$ f.\text{update}\,a\,b = f - \text{single}(a, f(a)) + \text{single}(a, b), $$ where $\text{single}(a, f(a))$ and $\text{single}(a, b)$ are the finitely supported functions that take the value $f(a)$ and $b$ at $a$ respectively, and zero elsewhere.

Finsupp.single_neg theorem

(a : α) (b : G) : single a (-b) = -single a b

Full source

@[simp]
theorem single_neg (a : α) (b : G) : single a (-b) = -single a b :=
  (singleAddHom a : G →+ _).map_neg b

Negation of Single-Point Finitely Supported Function: $\text{single}(a, -b) = -\text{single}(a, b)$

Informal description

For any element $a \in \alpha$ and any element $b$ in an additive group $G$, the finitely supported function that takes the value $-b$ at $a$ and zero elsewhere is equal to the negation of the finitely supported function that takes the value $b$ at $a$ and zero elsewhere. In other words, $\text{single}(a, -b) = -\text{single}(a, b)$.

Finsupp.single_sub theorem

(a : α) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂

Full source

@[simp]
theorem single_sub (a : α) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂ :=
  (singleAddHom a : G →+ _).map_sub b₁ b₂

Subtraction of Single-Point Finitely Supported Functions: $\operatorname{single}(a, b_1 - b_2) = \operatorname{single}(a, b_1) - \operatorname{single}(a, b_2)$

Informal description

For any element $a \in \alpha$ and any elements $b_1, b_2$ in an additive group $G$, the finitely supported function $\operatorname{single}(a, b_1 - b_2)$ is equal to the difference of the finitely supported functions $\operatorname{single}(a, b_1)$ and $\operatorname{single}(a, b_2)$. In other words: $$\operatorname{single}(a, b_1 - b_2) = \operatorname{single}(a, b_1) - \operatorname{single}(a, b_2).$$

Finsupp.erase_neg theorem

(a : α) (f : α →₀ G) : erase a (-f) = -erase a f

Full source

@[simp]
theorem erase_neg (a : α) (f : α →₀ G) : erase a (-f) = -erase a f :=
  (eraseAddHom a : (_ →₀ G) →+ _).map_neg f

Negation Commutes with Erasure in Finitely Supported Functions

Informal description

For any element $a \in \alpha$ and any finitely supported function $f \colon \alpha \to_{\text{f}} G$, the operation of erasing $a$ from the negation of $f$ is equal to the negation of erasing $a$ from $f$. That is, $\operatorname{erase}_a (-f) = -\operatorname{erase}_a f$.

Finsupp.erase_sub theorem

(a : α) (f₁ f₂ : α →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂

Full source

@[simp]
theorem erase_sub (a : α) (f₁ f₂ : α →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂ :=
  (eraseAddHom a : (_ →₀ G) →+ _).map_sub f₁ f₂

Erasure Preserves Subtraction of Finitely Supported Functions

Informal description

For any element $a \in \alpha$ and any two finitely supported functions $f_1, f_2 : \alpha \to_{\text{f}} G$, the erasure of their difference at $a$ equals the difference of their erasures at $a$, i.e., \[ \text{erase}_a (f_1 - f_2) = \text{erase}_a f_1 - \text{erase}_a f_2. \] Here, $\text{erase}_a f$ denotes the function that coincides with $f$ everywhere except at $a$, where it is set to $0$.

Mathlib.Data.Finsupp.Single

Main declarations

Implementation notes