mathlib documentation

data.dfinsupp.order

Pointwise order on finitely supported dependent functions #

This file lifts order structures on the α i to Π₀ i, α i.

Main declarations #

TODO #

Add is_well_order (Π₀ i, α i) (<).

Order structures #

@[protected, instance]
def dfinsupp.has_le {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), has_le (α i)] :
has_le (Π₀ (i : ι), α i)
Equations
theorem dfinsupp.le_def {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), has_le (α i)] {f g : Π₀ (i : ι), α i} :
f g ∀ (i : ι), f i g i
def dfinsupp.order_embedding_to_fun {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), has_le (α i)] :
(Π₀ (i : ι), α i) ↪o Π (i : ι), α i

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

Equations
@[simp]
theorem dfinsupp.order_embedding_to_fun_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), has_le (α i)] {f : Π₀ (i : ι), α i} {i : ι} :
@[protected, instance]
def dfinsupp.preorder {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] :
preorder (Π₀ (i : ι), α i)
Equations
theorem dfinsupp.coe_fn_mono {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] :
@[protected, instance]
def dfinsupp.partial_order {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] :
partial_order (Π₀ (i : ι), α i)
Equations
@[protected, instance]
def dfinsupp.semilattice_inf {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π₀ (i : ι), α i)
Equations
@[simp]
theorem dfinsupp.inf_apply {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), semilattice_inf (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
(f g) i = f i g i
@[protected, instance]
def dfinsupp.semilattice_sup {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π₀ (i : ι), α i)
Equations
@[simp]
theorem dfinsupp.sup_apply {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), semilattice_sup (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
(f g) i = f i g i
@[protected, instance]
def dfinsupp.lattice {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), has_zero (α i)] [Π (i : ι), lattice (α i)] :
lattice (Π₀ (i : ι), α i)
Equations

Algebraic order structures #

@[protected, instance]
def dfinsupp.has_le.le.contravariant_class {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), ordered_add_comm_monoid (α i)] [∀ (i : ι), contravariant_class (α i) (α i) has_add.add has_le.le] :
contravariant_class (Π₀ (i : ι), α i) (Π₀ (i : ι), α i) has_add.add has_le.le
@[protected, instance]
def dfinsupp.order_bot {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), canonically_ordered_add_monoid (α i)] :
order_bot (Π₀ (i : ι), α i)
Equations
@[protected]
theorem dfinsupp.bot_eq_zero {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] :
= 0
@[simp]
theorem dfinsupp.add_eq_zero_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] (f g : Π₀ (i : ι), α i) :
f + g = 0 f = 0 g = 0
theorem dfinsupp.le_iff' {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] {f g : Π₀ (i : ι), α i} {s : finset ι} (hf : f.support s) :
f g ∀ (i : ι), i sf i g i
theorem dfinsupp.le_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] {f g : Π₀ (i : ι), α i} :
f g ∀ (i : ι), i f.supportf i g i
@[protected, instance]
def dfinsupp.decidable_le {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), canonically_ordered_add_monoid (α i)] [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] [Π (i : ι), decidable_rel has_le.le] :
Equations
@[simp]
theorem dfinsupp.single_le_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :
@[protected, instance]
def dfinsupp.tsub {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] :
has_sub (Π₀ (i : ι), α i)

This is called tsub for truncated subtraction, to distinguish it with subtraction in an additive group.

Equations
theorem dfinsupp.tsub_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
(f - g) i = f i - g i
@[simp]
theorem dfinsupp.coe_tsub {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] (f g : Π₀ (i : ι), α i) :
(f - g) = f - g
@[protected, instance]
def dfinsupp.has_ordered_sub {ι : Type u_1} (α : ι → Type u_2) [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] :
has_ordered_sub (Π₀ (i : ι), α i)
Equations
@[simp]
theorem dfinsupp.single_tsub {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] {i : ι} {a b : α i} [decidable_eq ι] :
theorem dfinsupp.support_tsub {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] {f g : Π₀ (i : ι), α i} [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] :
theorem dfinsupp.subset_support_tsub {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), has_sub (α i)] [Π (i : ι), has_ordered_sub (α i)] {f g : Π₀ (i : ι), α i} [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] :
@[simp]
theorem dfinsupp.support_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_linear_ordered_add_monoid (α i)] [decidable_eq ι] {f g : Π₀ (i : ι), α i} :
@[simp]
theorem dfinsupp.support_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_linear_ordered_add_monoid (α i)] [decidable_eq ι] {f g : Π₀ (i : ι), α i} :
theorem dfinsupp.disjoint_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), canonically_linear_ordered_add_monoid (α i)] [decidable_eq ι] {f g : Π₀ (i : ι), α i} :