Documentation

Mathlib.Order.Preorder.Finsupp

Pointwise order on finitely supported functions #

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

source
🔸 coverage
@[implicit_reducible]
instance Finsupp.instLE {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] :
LE (ι →₀ M)
source
📐 coverage
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
source
📐 coverage
@[simp]
theorem Finsupp.coe_le_coe {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] {f g : ι →₀ M} :
⇑f ≤ ⇑g ↔ f ≤ g
source
🔸 coverage
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

Instances For
    source
    📐 coverage
    @[simp]
    theorem Finsupp.orderEmbeddingToFun_apply {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] (f : ι →₀ M) (a : ι) :
    orderEmbeddingToFun f a = f a
    source
    🔸 coverage
    noncomputable def Finsupp.orderIsoFunOnFinite {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] [Finite ι] :
    (ι →₀ M) ≃o (ι → M)

    equivFunOnFinite as an order isomorphism.

    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance Finsupp.preorder {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
      Preorder (ι →₀ M)
      source
      📐 coverage
      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
      source
      📐 coverage
      @[simp]
      theorem Finsupp.coe_lt_coe {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] {f g : ι →₀ M} :
      ⇑f < ⇑g ↔ f < g
      source
      📐 coverage
      theorem Finsupp.coe_mono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
      Monotone toFun
      source
      📐 coverage
      theorem Finsupp.coe_strictMono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
      Monotone toFun
      source
      🔸 coverage
      @[implicit_reducible]
      instance Finsupp.partialorder {ι : Type u_1} {M : Type u_2} [Zero M] [PartialOrder M] :
      PartialOrder (ι →₀ M)
      source
      🔸 coverage
      @[implicit_reducible]
      noncomputable instance Finsupp.semilatticeInf {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] :
      SemilatticeInf (ι →₀ M)
      source
      📐 coverage
      @[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
      source
      🔸 coverage
      @[implicit_reducible]
      noncomputable instance Finsupp.semilatticeSup {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] :
      SemilatticeSup (ι →₀ M)
      source
      📐 coverage
      @[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
      source
      🔸 coverage
      @[implicit_reducible]
      noncomputable instance Finsupp.lattice {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] :
      Lattice (ι →₀ M)
      source
      📐 coverage
      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
      source
      📐 coverage
      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