Documentation

Cslib.Foundations.Data.FinFun

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.

source
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.

Instances For
    source
    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
    Instances For
      source
      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
      Instances For
        source
        instance Cslib.FinFun.instFunLike {β : Type u_1} {α : Type u_2} [Zero β] :
        FunLike (FinFun α β) α β
        Equations
        source
        theorem Cslib.FinFun.coe_fn {β : Type u_1} {α : Type u_2} [Zero β] {f : FinFun α β} :
        ⇑f = f.fn
        source
        theorem Cslib.FinFun.coe_eq_fn {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} :
        f a = f.fn a
        source
        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.

        source
        theorem Cslib.FinFun.mem_support_not_zero {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} :
        a ∈ f.support ↔ f a ≠ 0
        source
        theorem Cslib.FinFun.not_mem_support_zero {β : Type u_1} {α : Type u_2} {a : α} [Zero β] {f : FinFun α β} :
        a ∉ f.support ↔ f a = 0
        source
        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.

        source
        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.

        source
        theorem Cslib.FinFun.congrFinFun {β : Type u_1} {α : Type u_2} [Zero β] {f g : FinFun α β} (h : f = g) (a : α) :
        f a = g a
        source
        theorem Cslib.FinFun.fromFun_eq {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) (h : ∀ a ∉ support, f a = 0) :
        ⇑(Cslib.FinFun.fromFun✝ f support) = f
        source
        theorem Cslib.FinFun.fromFun_fn {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) :
        (Cslib.FinFun.fromFun✝ f support).fn = fun (a : α) => if a ∈ support then f a else 0
        source
        theorem Cslib.FinFun.fromFun_support {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] (f : α → β) (support : Finset α) :
        (Cslib.FinFun.fromFun✝ f support).support = Finset.filter (fun (x : α) => f x ≠ 0) support
        source
        theorem Cslib.FinFun.fromFun_idem {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [(y : β) → Decidable (y = 0)] {f : α → β} {support : Finset α} :
        Cslib.FinFun.fromFun✝ (⇑(Cslib.FinFun.fromFun✝¹ f support)) support = Cslib.FinFun.fromFun✝² f support

        Restricting a function twice to the same support is idempotent.

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

        Restricting a FinFun to its own support is the identity.

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

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

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

        Restricting a function is commutative.