Finite functions

Given types α and β, and assuming that β has a Zero element, a FinFun α β is a function from α to β where only a finite number of elements in α are mapped to non-zero elements.

structure Cslib.FinFun (α : Type u_1) (β : Type u_2) [Zero β] : Type (max u_1 u_2)

A FinFun is a function fn with a finite support.

This is similar to Finsupp in Mathlib, but definitions are computable.

• fn : α → β

  The underlying function.

• support : Finset α

  The finite support of the function.

• mem_support_fn {a : α} : a ∈ self.support ↔ self.fn a ≠ 0

  Proof that support is the support of the underlying function.

def Cslib.FinFun.«term_→₀_» : Lean.TrailingParserDescr

A FinFun is a function fn with a finite support.

This is similar to Finsupp in Mathlib, but definitions are computable.

Equations

• Cslib.FinFun.«term_→₀_» = Lean.ParserDescr.trailingNode `Cslib.FinFun.«term_→₀_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →₀ ") (Lean.ParserDescr.cat `term 25))

def Cslib.FinFun.fromFun {α : Type u_1} {β : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (fn : α → β) (support : Finset α) : FinFun α β

Constructs a FinFun by restricting a function to a given support, filtering out all elements not mapped to 0 in the support.

Equations

• Cslib.FinFun.fromFun fn support = { fn := fun (a : α) => if a ∈ support then fn a else 0, support := Finset.filter (fun (x : α) => fn x ≠ 0) support, mem_support_fn := ⋯ }

def Cslib.FinFun.«term_↾₀_» : Lean.TrailingParserDescr

Constructs a FinFun by restricting a function to a given support, filtering out all elements not mapped to 0 in the support.

Equations

• Cslib.FinFun.«term_↾₀_» = Lean.ParserDescr.trailingNode `Cslib.FinFun.«term_↾₀_» 1022 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾₀") (Lean.ParserDescr.cat `term 51))

instance Cslib.FinFun.instFunLike {β : Type u_1} {α : Type u_2} [Zero β] : FunLike (FinFun α β) α β

Equations

• Cslib.FinFun.instFunLike = { coe := fun (f : Cslib.FinFun α β) => f.fn, coe_injective' := ⋯ }

theorem Cslib.FinFun.coe_fn {β : Type u_1} {α : Type u_2} [Zero β] {f : FinFun α β} : ⇑f = f.fn

theorem Cslib.FinFun.coe_eq_fn {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} : f a = f.fn a

theorem Cslib.FinFun.ext {β : Type u_1} {α : Type u_2} [Zero β] {f g : FinFun α β} (h : ∀ (a : α), f a = g a) : f = g

Extensional equality for FinFun.

theorem Cslib.FinFun.mem_support_not_zero {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} : a ∈ f.support ↔ f a ≠ 0

theorem Cslib.FinFun.not_mem_support_zero {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} : ¬a ∈ f.support ↔ f a = 0

theorem Cslib.FinFun.eq_fields_eq {β : Type u_1} {α : Type u_2} [Zero β] {f g : FinFun α β} : f = g → f.fn = g.fn ∧ f.support = g.support

If two FinFuns are equal, their underlying functions and supports are equal.

theorem Cslib.FinFun.fn_eq_eq {β : Type u_1} {α : Type u_2} [Zero β] {f g : FinFun α β} (h : f.fn = g.fn) : f = g

If two functions are equal, two FinFuns respectively using them as underlying functions are equal.

theorem Cslib.FinFun.congrFinFun {β : Type u_1} {α : Type u_2} [Zero β] {f g : FinFun α β} (h : f = g) (a : α) : f a = g a

theorem Cslib.FinFun.fromFun_eq {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) (h : ∀ (a : α), ¬a ∈ support → f a = 0) : ⇑(fromFun f support) = f

theorem Cslib.FinFun.fromFun_fn {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) : (fromFun f support).fn = fun (a : α) => if a ∈ support then f a else 0

theorem Cslib.FinFun.fromFun_support {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) : (fromFun f support).support = Finset.filter (fun (x : α) => f x ≠ 0) support

theorem Cslib.FinFun.fromFun_idem {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] {f : α → β} {support : Finset α} : fromFun (⇑(fromFun f support)) support = fromFun f support

Restricting a function twice to the same support is idempotent.

theorem Cslib.FinFun.coe_fromFun_id {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] {f : FinFun α β} : fromFun (⇑f) f.support = f

Restricting a FinFun to its own support is the identity.

theorem Cslib.FinFun.fromFun_inter {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} : fromFun (⇑(fromFun f support1)) support2 = fromFun f (support1 ∩ support2)

Restricting a function twice to two supports is equal to restricting to their intersection.

theorem Cslib.FinFun.fromFun_comm {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} : fromFun (⇑(fromFun f support1)) support2 = fromFun (⇑(fromFun f support2)) support1

Restricting a function is commutative.