Pointwise order on finitely supported functions

This file lifts order structures on M to ι →₀ M.

instance Finsupp.instLE {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] : LE (ι →₀ M)

Equations

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

theorem Finsupp.le_def {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] {f g : ι →₀ M} : f ≤ g ↔ ∀ (i : ι), f i ≤ g i

@[simp]

theorem Finsupp.coe_le_coe {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] {f g : ι →₀ M} : ⇑f ≤ ⇑g ↔ f ≤ g

def Finsupp.orderEmbeddingToFun {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] : (ι →₀ M) ↪o (ι → M)

The order on Finsupps over a partial order embeds into the order on functions

Equations

• Finsupp.orderEmbeddingToFun = { toFun := fun (f : ι →₀ M) => ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Finsupp.orderEmbeddingToFun_apply {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] (f : ι →₀ M) (a : ι) : orderEmbeddingToFun f a = f a

instance Finsupp.preorder {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] : Preorder (ι →₀ M)

Equations

• Finsupp.preorder = { toLE := Finsupp.instLE, lt := fun (a b : ι →₀ M) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Finsupp.lt_def {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] {f g : ι →₀ M} : f < g ↔ f ≤ g ∧ ∃ (i : ι), f i < g i

@[simp]

theorem Finsupp.coe_lt_coe {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] {f g : ι →₀ M} : ⇑f < ⇑g ↔ f < g

theorem Finsupp.coe_mono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] : Monotone toFun

theorem Finsupp.coe_strictMono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] : Monotone toFun

instance Finsupp.partialorder {ι : Type u_1} {M : Type u_2} [Zero M] [PartialOrder M] : PartialOrder (ι →₀ M)

Equations

• Finsupp.partialorder = { toPreorder := Finsupp.preorder, le_antisymm := ⋯ }

instance Finsupp.semilatticeInf {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] : SemilatticeInf (ι →₀ M)

Equations

• Finsupp.semilatticeInf = { toPartialOrder := Finsupp.partialorder, inf := Finsupp.zipWith (fun (x1 x2 : M) => x1 ⊓ x2) ⋯, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[simp]

theorem Finsupp.inf_apply {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] (f g : ι →₀ M) (i : ι) : (f ⊓ g) i = f i ⊓ g i

instance Finsupp.semilatticeSup {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] : SemilatticeSup (ι →₀ M)

Equations

• Finsupp.semilatticeSup = { toPartialOrder := Finsupp.partialorder, sup := Finsupp.zipWith (fun (x1 x2 : M) => x1 ⊔ x2) ⋯, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[simp]

theorem Finsupp.sup_apply {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] (f g : ι →₀ M) (i : ι) : (f ⊔ g) i = f i ⊔ g i

instance Finsupp.lattice {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] : Lattice (ι →₀ M)

Equations

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

theorem Finsupp.support_inf_union_support_sup {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] (f g : ι →₀ M) [DecidableEq ι] : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support

theorem Finsupp.support_sup_union_support_inf {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] (f g : ι →₀ M) [DecidableEq ι] : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support