Finite Functions

Note: the API and notation of FinFun is still unstable.

A FinFun α β is a function from α to β with a finite domain of definition.

structure FinFun (α : Type u) (β : Type v) : Type (max u v)

A finite function FinFun is a function f equipped with a domain of definition dom.

• f : α → β
• dom : Finset α

def «term_⇀_» : Lean.TrailingParserDescr

Equations

• «term_⇀_» = Lean.ParserDescr.trailingNode `«term_⇀_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇀ ") (Lean.ParserDescr.cat `term 0))

def «term_↾_» : Lean.TrailingParserDescr

Equations

• «term_↾_» = Lean.ParserDescr.trailingNode `«term_↾_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 0))

@[reducible, inline]

abbrev CompleteDom {β : Type u_1} {α : Type u_2} [Zero β] (f : α ⇀ β) : Prop

Equations

• CompleteDom f = ∀ x ∉ f.dom, f.f x = 0

def FinFun.defined {α : Type u_1} {β : Type u_2} (f : α ⇀ β) (x : α) : Prop

Equations

• f.defined x = (x ∈ f.dom)

@[reducible, inline]

abbrev FinFun.apply {α : Type u_1} {β : Type u_2} (f : α ⇀ β) (x : α) : β

Equations

• f.apply x = f.f x

def FinFun.toFun {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] (f : α ⇀ β) : α → β

Equations

• ↑f x = if x ∈ f.dom then f.f x else Zero.zero

instance instCoeFinFunForallOfDecidableEqOfZero {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] : Coe (α ⇀ β) (α → β)

Equations

• instCoeFinFunForallOfDecidableEqOfZero = { coe := FinFun.toFun }

theorem FinFun.toFun_char {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] {f g : α ⇀ β} (h : ↑f = ↑g) (x : α) : (x ∈ f.dom ∩ g.dom → f.apply x = g.apply x) ∧ (x ∈ f.dom \ g.dom → f.apply x = Zero.zero) ∧ (x ∈ g.dom \ f.dom → g.apply x = Zero.zero)

theorem FinFun.toFun_dom {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] {f : α ⇀ β} (h : ∀ x ∉ f.dom, f.apply x = Zero.zero) : ↑f = f.f

def FinFun.mapBin {α : Type u_1} {β : Type u_2} [DecidableEq α] (f g : α ⇀ β) (op : Option β → Option β → Option β) : Option (α ⇀ β)

Equations

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

theorem FinFun.mapBin_dom {α : Type u_1} {β : Type u_2} {fg : α ⇀ β} [DecidableEq α] (f g : α ⇀ β) (op : Option β → Option β → Option β) (h : f.mapBin g op = some fg) : fg.dom = f.dom ∧ fg.dom = g.dom

theorem FinFun.mapBin_char₁ {α : Type u_1} {β : Type u_2} {fg : α ⇀ β} {y : β} [DecidableEq α] (f g : α ⇀ β) (op : Option β → Option β → Option β) (h : f.mapBin g op = some fg) (x : α) : x ∈ fg.dom → (fg.apply x = y ↔ op (some (f.f x)) (some (g.f x)) = some y)

theorem FinFun.mapBin_char₂ {α : Type u_1} {β : Type u_2} [DecidableEq α] (f g : α ⇀ β) (op : Option β → Option β → Option β) (hdom : f.dom = g.dom) (hop : ∀ x ∈ f.dom, (op (some (f.f x)) (some (g.f x))).isSome = true) : (f.mapBin g op).isSome = true

def Function.toFinFun {α : Type u_1} {β : Type u_2} [DecidableEq α] (f : α → β) (dom : Finset α) : α ⇀ β

Equations

• Function.toFinFun f dom = (f↾dom)

theorem Function.toFinFun_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] (f : α → β) (dom : Finset α) (h : ∀ x ∉ dom, f x = 0) : f = ↑(toFinFun f dom)

def FinFun.toDomFun {α : Type u_1} {β : Type u_2} (f : α ⇀ β) : { x : α // x ∈ f.dom } → β

Equations

• ↑f x = f.f ↑x

theorem FinFun.toDomFun_char {α : Type u_1} {β : Type u_2} {x : α} (f : α ⇀ β) (h : x ∈ f.dom) : ↑f ⟨x, h⟩ = f.f x

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

theorem FinFun.eq_char₁ {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] {f g : α ⇀ β} (h : f = g) : f.f = g.f ∧ f.dom = g.dom

theorem FinFun.eq_char₂ {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] {f g : α ⇀ β} (heq : f.f = g.f ∧ f.dom = g.dom) : f = g

theorem FinFun.eq_char {α : Type u_1} {β : Type u_2} [DecidableEq α] [Zero β] {f g : α ⇀ β} : f = g ↔ f.f = g.f ∧ f.dom = g.dom