data.finsupp.lattice - mathlib docs

source

@[protected, instance]

def finsupp.order_bot {α : Type u_1} {μ : Type u_3} [canonically_ordered_add_monoid μ] :

order_bot (α →₀ μ)

Equations

finsupp.order_bot = {bot := 0, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[protected, instance]

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

semilattice_inf (α →₀ β)

Equations

finsupp.semilattice_inf = {inf := finsupp.zip_with has_inf.inf finsupp.semilattice_inf._proof_1, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[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

source

@[simp]

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

(f ⊓ g).support = f.support ∩ g.support

source

@[protected, instance]

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

semilattice_sup (α →₀ β)

Equations

finsupp.semilattice_sup = {sup := finsupp.zip_with has_sup.sup finsupp.semilattice_sup._proof_1, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[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

source

@[simp]

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

(f ⊔ g).support = f.support ∪ g.support

source

@[protected, instance]

def finsupp.lattice {α : Type u_1} {β : Type u_2} [has_zero β] [lattice β] :

lattice (α →₀ β)

Equations

finsupp.lattice = {sup := semilattice_sup.sup finsupp.semilattice_sup, le := semilattice_inf.le finsupp.semilattice_inf, lt := semilattice_inf.lt finsupp.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf finsupp.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def finsupp.semilattice_inf_bot {α : Type u_1} {γ : Type u_4} [canonically_linear_ordered_add_monoid γ] :

semilattice_inf_bot (α →₀ γ)

Equations

finsupp.semilattice_inf_bot = {bot := order_bot.bot finsupp.order_bot, le := order_bot.le finsupp.order_bot, lt := order_bot.lt finsupp.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := lattice.inf finsupp.lattice, inf_le_left := _, inf_le_right := _, le_inf := _}

source

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

⊥ = 0

source

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

disjoint x y ↔ disjoint x.support y.support

source

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

finsupp.order_embedding_to_fun = {to_embedding := {to_fun := λ (f : α →₀ β) (a : α), ⇑f a, inj' := _}, map_rel_iff' := _}

source

@[simp]

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

⇑finsupp.order_embedding_to_fun f a = ⇑f a

source

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

monotone finsupp.to_fun

mathlib documentation

Lattice structure on finsupps #