Documentation

Mathlib.Order.Preorder.Finsupp

Pointwise order on finitely supported functions #

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

source
🔸 coverage
instance Finsupp.instLE {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] :
LE (ι →₀ M)
Equations
    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

    Equations
      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
        def Finsupp.orderIsoFunOnFinite {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] [Finite ι] :
        (ι →₀ M) ≃o (ι → M)

        equivFunOnFinite as an order isomorphism.

        Equations
          Instances For
            source
            🔸 coverage
            instance Finsupp.preorder {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
            Preorder (ι →₀ M)
            Equations
              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
              instance Finsupp.partialorder {ι : Type u_1} {M : Type u_2} [Zero M] [PartialOrder M] :
              PartialOrder (ι →₀ M)
              Equations
                source
                🔸 coverage
                instance Finsupp.semilatticeInf {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] :
                SemilatticeInf (ι →₀ M)
                Equations
                  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
                  instance Finsupp.semilatticeSup {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] :
                  SemilatticeSup (ι →₀ M)
                  Equations
                    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
                    instance Finsupp.lattice {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] :
                    Lattice (ι →₀ M)
                    Equations
                      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