def Finsupp.η' {X α : Type} [DecidableEq X] [DecidableEq α] [Zero α] [One α] (x : X) : X →₀ α

Equations

• Finsupp.η' x = { support := if 1 = 0 then ∅ else {x}, toFun := fun (y : X) => if x = y then 1 else 0, mem_support_toFun := ⋯ }

def Finsupp.«termη'[_]» : Lean.ParserDescr

Equations

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

@[simp]

theorem Finsupp.η'_apply {X α : Type} [DecidableEq X] [DecidableEq α] [Zero α] [One α] (x y : X) : (η' x) y = if x = y then 1 else 0

@[simp]

theorem Finsupp.η'_finSupp {X α : Type} [DecidableEq X] [DecidableEq α] [Zero α] [One α] (x : X) : (η' x).support = if 1 = 0 then ∅ else {x}

@[implicit_reducible]

instance Finsupp.instOne {α X : Type} [Fintype X] [Zero α] [One α] [DecidableEq α] : One (X →₀ α)

Equations

• Finsupp.instOne = { one := { support := if 1 = 0 then ∅ else Fintype.elems, toFun := fun (x : X) => 1, mem_support_toFun := ⋯ } }

@[simp]

theorem Finsupp.one_apply {α X : Type} [Fintype X] [Zero α] [One α] [DecidableEq α] {x : X} : 1 x = 1

def Finsupp.zipWith' {α M N P : Type} [Zero M] [Zero N] [Zero P] [DecidableEq α] [DecidableEq P] (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P

Given finitely supported functions g₁ : α →₀ M and g₂ : α →₀ N and function f : M → N → P, Finsupp.zipWith f hf g₁ g₂ is the finitely supported function α →₀ P satisfying zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a), which is well-defined when f 0 0 = 0.

Equations

• Finsupp.zipWith' f hf g₁ g₂ = { support := {x ∈ g₁.support ∪ g₂.support | f (g₁ x) (g₂ x) ≠ 0}, toFun := fun (x : α) => f (g₁ x) (g₂ x), mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.zipWith'_apply {α M N P : Type} [Zero M] [Zero N] [Zero P] [DecidableEq α] [DecidableEq P] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} : (zipWith' f hf g₁ g₂) a = f (g₁ a) (g₂ a)

theorem Finsupp.support_zipWith' {α M N P : Type} [Zero M] [Zero N] [Zero P] [DecidableEq α] [DecidableEq P] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} : (zipWith' f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

@[implicit_reducible, instance 10000]

instance Finsupp.instAdd' {ι M : Type} [AddZeroClass M] [DecidableEq ι] [DecidableEq M] : Add (ι →₀ M)

Equations

• Finsupp.instAdd' = { add := Finsupp.zipWith' (fun (x1 x2 : M) => x1 + x2) ⋯ }

@[simp]

theorem Finsupp.coe_add' {ι M : Type} [AddZeroClass M] [DecidableEq ι] [DecidableEq M] (f g : ι →₀ M) : ⇑(f + g) = ⇑f + ⇑g

@[implicit_reducible]

instance Finsupp.instAddZeroClass' {ι M : Type} [AddZeroClass M] [DecidableEq ι] [DecidableEq M] : AddZeroClass (ι →₀ M)

Equations

• Finsupp.instAddZeroClass' = Function.Injective.addZeroClass (fun (f : ι →₀ M) => ⇑f) ⋯ ⋯ ⋯

instance Finsupp.instIsLeftCancelAdd' {ι M : Type} [AddZeroClass M] [DecidableEq ι] [DecidableEq M] [IsLeftCancelAdd M] : IsLeftCancelAdd (ι →₀ M)

@[implicit_reducible]

instance Finsupp.instMul_weightedNetKAT {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] : Mul (α →₀ β)

The product of f g : α →₀ β is the finitely supported function whose value at a is f a * g a.

Equations

• Finsupp.instMul_weightedNetKAT = { mul := Finsupp.zipWith' (fun (x1 x2 : β) => x1 * x2) ⋯ }

theorem Finsupp.coe_mul {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] (g₁ g₂ : α →₀ β) : ⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂

@[simp]

theorem Finsupp.mul_apply {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] {g₁ g₂ : α →₀ β} {a : α} : (g₁ * g₂) a = g₁ a * g₂ a

theorem Finsupp.support_mul_subset_left {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support

theorem Finsupp.support_mul_subset_right {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₂.support

theorem Finsupp.support_mul {α β : Type} [MulZeroClass β] [DecidableEq β] [DecidableEq α] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support

@[implicit_reducible]

instance Finsupp.instMulZeroClass_weightedNetKAT {α β : Type} [MulZeroClass β] [DecidableEq α] [DecidableEq β] : MulZeroClass (α →₀ β)

Equations

• Finsupp.instMulZeroClass_weightedNetKAT = Function.Injective.mulZeroClass (fun (f : α →₀ β) => ⇑f) ⋯ ⋯ ⋯

@[implicit_reducible]

instance Finsupp.instHMul_weightedNetKAT {α β : Type} [MulZeroClass β] [DecidableEq β] : HMul β (α →₀ β) (α →₀ β)

Equations

• Finsupp.instHMul_weightedNetKAT = { hMul := fun (s : β) (f : α →₀ β) => { support := {x ∈ f.support | s * f x ≠ 0}, toFun := fun (x : α) => s * f x, mem_support_toFun := ⋯ } }

@[implicit_reducible]

instance Finsupp.instHMul_weightedNetKAT_1 {α β : Type} [MulZeroClass β] [DecidableEq β] : HMul (α →₀ β) β (α →₀ β)

Equations

• Finsupp.instHMul_weightedNetKAT_1 = { hMul := fun (f : α →₀ β) (s : β) => { support := {x ∈ f.support | f x * s ≠ 0}, toFun := fun (x : α) => f x * s, mem_support_toFun := ⋯ } }

theorem Finsupp.coe_hMul_left {α β : Type} [MulZeroClass β] [DecidableEq β] (s : β) (g : α →₀ β) : ⇑(s * g) = ⇑(s * g)

@[simp]

theorem Finsupp.hMul_left_apply {α β : Type} [MulZeroClass β] [DecidableEq β] {s : β} {g : α →₀ β} {a : α} : (s * g) a = s * g a

theorem Finsupp.support_hMul_left_subset_right {α β : Type} [MulZeroClass β] [DecidableEq β] {s : β} {g : α →₀ β} : (s * g).support ⊆ g.support

theorem Finsupp.support_hMul_left {α β : Type} [MulZeroClass β] [DecidableEq β] [DecidableEq α] {s : β} {g : α →₀ β} : (s * g).support ⊆ g.support

theorem Finsupp.coe_hMul_right {α β : Type} [MulZeroClass β] [DecidableEq β] (s : β) (g : α →₀ β) : ⇑(g * s) = ⇑(g * s)

@[simp]

theorem Finsupp.hMul_right_apply {α β : Type} [MulZeroClass β] [DecidableEq β] {s : β} {g : α →₀ β} {a : α} : (g * s) a = g a * s

theorem Finsupp.support_hMul_right_subset_right {α β : Type} [MulZeroClass β] [DecidableEq β] {s : β} {g : α →₀ β} : (g * s).support ⊆ g.support

theorem Finsupp.support_hMul_right {α β : Type} [MulZeroClass β] [DecidableEq β] [DecidableEq α] {s : β} {g : α →₀ β} : (g * s).support ⊆ g.support

@[implicit_reducible]

instance Finsupp.instLE_weightedNetKAT {M : Type} [Semiring M] [PartialOrder M] {ι : Type} : LE (ι →₀ M)

Equations

• Finsupp.instLE_weightedNetKAT = { le := fun (f g : ι →₀ M) => ∀ (x : ι), f x ≤ g x }

@[implicit_reducible]

instance Finsupp.instDecidableForallForallMemFinsetSupportOfDecidablePred_weightedNetKAT {M : Type} [Semiring M] {ι : Type} [DecidableEq ι] {f : ι →₀ M} {p : ι → Prop} [DecidablePred p] : Decidable (∀ x ∈ f.support, p x)

Equations

• Finsupp.instDecidableForallForallMemFinsetSupportOfDecidablePred_weightedNetKAT = if h : Finset.filter p f.support = f.support then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Finsupp.instPartialOrder_weightedNetKAT {M : Type} [Semiring M] [PartialOrder M] {ι : Type} : PartialOrder (ι →₀ M)

Equations

• Finsupp.instPartialOrder_weightedNetKAT = { toLE := Finsupp.instLE_weightedNetKAT, toLT := Finsupp.preorder.toLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance Finsupp.instOrderBot_weightedNetKAT {M : Type} [Semiring M] [PartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} : OrderBot (ι →₀ M)

Equations

• Finsupp.instOrderBot_weightedNetKAT = { bot := 0, bot_le := ⋯ }

instance Finsupp.instMulLeftMono_weightedNetKAT {M : Type} [Semiring M] [PartialOrder M] [MulLeftMono M] {ι : Type} [DecidableEq ι] [DecidableEq M] : MulLeftMono (ι →₀ M)

instance Finsupp.instMulRightMono_weightedNetKAT {M : Type} [Semiring M] [PartialOrder M] [MulRightMono M] {ι : Type} [DecidableEq ι] [DecidableEq M] : MulRightMono (ι →₀ M)

@[implicit_reducible]

instance Finsupp.instAddCommMonoid_weightedNetKAT {M : Type} [Semiring M] {ι : Type} [DecidableEq ι] [DecidableEq M] : AddCommMonoid (ι →₀ M)

Equations

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

@[simp]

theorem Finsupp.sum_apply''' {M : Type} [Semiring M] {ι : Type} [DecidableEq ι] [DecidableEq M] {Y : Type} [DecidableEq Y] {S : Finset ι} {f : ι → Y →₀ M} {a : Y} : (∑ x ∈ S, f x) a = ∑ x ∈ S, (f x) a

instance Finsupp.instIsPositiveOrderedAddMonoid {M : Type} [Semiring M] [PartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} [DecidableEq ι] [DecidableEq M] : IsPositiveOrderedAddMonoid (ι →₀ M)

@[implicit_reducible]

instance Finsupp.instNonUnitalSemiring_weightedNetKAT {M : Type} [Semiring M] {ι : Type} [DecidableEq ι] [DecidableEq M] : NonUnitalSemiring (ι →₀ M)

Equations

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

def Finsupp.bind {M : Type} [Semiring M] [PartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι Y : Type} [DecidableEq M] [DecidableEq Y] (f : ι →₀ M) (g : ι → Y →₀ M) : Y →₀ M

Equations

• f.bind g = { support := f.support.biUnion fun (x : ι) => {y ∈ (g x).support | f x * (g x) y ≠ 0}, toFun := fun (y : Y) => ∑ x : ↥f.support, f ↑x * (g ↑x) y, mem_support_toFun := ⋯ }

@[implicit_reducible]

instance Finsupp.instOmegaCompletePartialOrderOfFintype_weightedNetKAT {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} [DecidableEq M] [Fintype ι] : OmegaCompletePartialOrder (ι →₀ M)

Equations

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

@[simp]

theorem Finsupp.ωSup_apply {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} [Fintype ι] [DecidableEq M] (C : OmegaCompletePartialOrder.Chain (ι →₀ M)) (x : ι) : (OmegaCompletePartialOrder.ωSup C) x = OmegaCompletePartialOrder.ωSup (C.map { toFun := fun (x_1 : ι →₀ M) => x_1 x, monotone' := ⋯ })

instance Finsupp.instOmegaContinuousNonUnitalSemiring {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [MulLeftMono M] [MulRightMono M] [IsPositiveOrderedAddMonoid M] [OmegaContinuousNonUnitalSemiring M] {ι : Type} [DecidableEq ι] [DecidableEq M] [Fintype ι] : OmegaContinuousNonUnitalSemiring (ι →₀ M)

@[simp]

theorem Finsupp.ωSum_apply {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} [DecidableEq M] [Countable ι] {Y : Type} [DecidableEq Y] [Fintype Y] {f : ι → Y →₀ M} {y : Y} : (ω∑ (x : ι), f x) y = ω∑ (x : ι), (f x) y