mathlib documentation

data.finsupp.lattice

Lattice structure on finsupps

This file provides instances of ordered structures on finsupps.

@[instance]
def finsupp.semilattice_inf {α : Type u_1} {β : Type u_2} [has_zero β] [semilattice_inf β] :

Equations
@[simp]
theorem finsupp.inf_apply {α : Type u_1} {β : Type u_2} [has_zero β] [semilattice_inf β] {a : α} {f g : α →₀ β} :
(f g) a = f a g a

@[simp]
theorem finsupp.support_inf {α : Type u_1} {γ : Type u_4} [canonically_linear_ordered_add_monoid γ] {f g : α →₀ γ} :

@[instance]
def finsupp.semilattice_sup {α : Type u_1} {β : Type u_2} [has_zero β] [semilattice_sup β] :

Equations
@[simp]
theorem finsupp.sup_apply {α : Type u_1} {β : Type u_2} [has_zero β] [semilattice_sup β] {a : α} {f g : α →₀ β} :
(f g) a = f a g a

@[simp]
theorem finsupp.support_sup {α : Type u_1} {γ : Type u_4} [canonically_linear_ordered_add_monoid γ] {f g : α →₀ γ} :

theorem finsupp.bot_eq_zero {α : Type u_1} {γ : Type u_4} [canonically_linear_ordered_add_monoid γ] :
= 0

theorem finsupp.disjoint_iff {α : Type u_1} {γ : Type u_4} [canonically_linear_ordered_add_monoid γ] {x y : α →₀ γ} :

def finsupp.order_embedding_to_fun {α : Type u_1} {β : Type u_2} [has_zero β] [partial_order β] :
→₀ β) ↪o (α → β)

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

Equations
@[simp]
theorem finsupp.order_embedding_to_fun_apply {α : Type u_1} {β : Type u_2} [has_zero β] [partial_order β] {f : α →₀ β} {a : α} :

theorem finsupp.monotone_to_fun {α : Type u_1} {β : Type u_2} [has_zero β] [partial_order β] :