feat(library/algebra/order_bigops): add min and max over finsets and finite sets
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
53b2d90c90
commit
27865e1c8b
2 changed files with 478 additions and 0 deletions
|
|
@ -22,5 +22,6 @@ Algebraic structures.
|
|||
* [module](module.lean) : modules, vector spaces, and linear maps
|
||||
* [ring_power](ring_power.lean) : power in ring structures
|
||||
* [ring_bigops](ring_bigops.lean) : products and sums in various structures
|
||||
* [order_bigops](order_bigops.lean) : min and max over finsets and finite sets
|
||||
* [bundled](bundled.lean) : bundled versions of the algebraic structures
|
||||
* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)
|
||||
|
|
|
|||
477
library/algebra/order_bigops.lean
Normal file
477
library/algebra/order_bigops.lean
Normal file
|
|
@ -0,0 +1,477 @@
|
|||
/-
|
||||
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Jeremy Avigad
|
||||
|
||||
Min and max over finite sets.
|
||||
|
||||
To support constructive theories, we start with the class
|
||||
decidable_linear_ordered_cancel_comm_monoid, because:
|
||||
(1) We need a decidable linear order to have min and max
|
||||
(2) We need a default element for min and max over the empty set, and max empty = 0 is the
|
||||
right choice for nat.
|
||||
(3) All our number classes are instances.
|
||||
We can define variants of Min and Max if needed.
|
||||
-/
|
||||
import .group_bigops .ordered_ring
|
||||
|
||||
variables {A B : Type}
|
||||
|
||||
section
|
||||
variable [decidable_linear_order A]
|
||||
|
||||
definition max_comm_semigroup : comm_semigroup A :=
|
||||
⦃ comm_semigroup,
|
||||
mul := max,
|
||||
mul_assoc := max.assoc,
|
||||
mul_comm := max.comm
|
||||
⦄
|
||||
|
||||
definition min_comm_semigroup : comm_semigroup A :=
|
||||
⦃ comm_semigroup,
|
||||
mul := min,
|
||||
mul_assoc := min.assoc,
|
||||
mul_comm := min.comm
|
||||
⦄
|
||||
end
|
||||
|
||||
/- finset versions -/
|
||||
|
||||
namespace finset
|
||||
|
||||
section deceq_A
|
||||
variable [decidable_eq A]
|
||||
|
||||
section decidable_linear_ordered_cancel_comm_monoid_B
|
||||
variable [decidable_linear_ordered_cancel_comm_monoid B]
|
||||
|
||||
section max_comm_semigroup
|
||||
local attribute max_comm_semigroup [instance]
|
||||
open Prod_semigroup
|
||||
|
||||
definition Max (s : finset A) (f : A → B) : B := Prod_semigroup 0 s f
|
||||
notation `Max` binders `∈` s `, ` r:(scoped f, Max s f) := r
|
||||
|
||||
proposition Max_empty (f : A → B) : (Max x ∈ ∅, f x) = 0 := !Prod_semigroup_empty
|
||||
|
||||
proposition Max_singleton (f : A → B) (a : A) : (Max x ∈ '{a}, f x) = f a :=
|
||||
!Prod_semigroup_singleton
|
||||
|
||||
proposition Max_insert_insert (f : A → B) {a₁ a₂ : A} {s : finset A} :
|
||||
a₂ ∉ s → a₁ ∉ insert a₂ s →
|
||||
(Max x ∈ insert a₁ (insert a₂ s), f x) = max (f a₁) (Max x ∈ insert a₂ s, f x) :=
|
||||
!Prod_semigroup_insert_insert
|
||||
|
||||
proposition Max_insert (f : A → B) {a : A} {s : finset A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
(Max x ∈ insert a s, f x) = max (f a) (Max x ∈ s, f x) :=
|
||||
!Prod_semigroup_insert anins sne
|
||||
end max_comm_semigroup
|
||||
|
||||
proposition Max_pair (f : A → B) (a₁ a₂ : A) : (Max x ∈ '{a₁, a₂}, f x) = max (f a₁) (f a₂) :=
|
||||
decidable.by_cases
|
||||
(suppose a₁ = a₂, by rewrite [this, pair_eq_singleton, max_self] )
|
||||
(suppose a₁ ≠ a₂,
|
||||
have a₁ ∉ '{a₂}, by rewrite [mem_singleton_iff]; apply this,
|
||||
using this, by rewrite [Max_insert f this !singleton_ne_empty])
|
||||
|
||||
proposition le_Max (f : A → B) {a : A} {s : finset A} (H : a ∈ s) : f a ≤ Max x ∈ s, f x :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact false.elim (not_mem_empty a H)},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'nempty,
|
||||
{rewrite [s'empty at *, Max_singleton, eq_of_mem_singleton H], apply le.refl},
|
||||
rewrite [Max_insert f a'nins' s'nempty],
|
||||
cases (eq_or_mem_of_mem_insert H) with aeqa' ains',
|
||||
{rewrite aeqa', apply le_max_left},
|
||||
apply le.trans (ih ains') !le_max_right
|
||||
end
|
||||
|
||||
proposition Max_le (f : A → B) {s : finset A} {b : B} (sne : s ≠ ∅) (H : ∀ a, a ∈ s → f a ≤ b) :
|
||||
(Max x ∈ s, f x) ≤ b :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'nempty,
|
||||
{rewrite [s'empty, Max_singleton], exact H a' !mem_insert},
|
||||
rewrite [Max_insert f a'nins' s'nempty],
|
||||
apply max_le (H a' !mem_insert),
|
||||
apply ih s'nempty,
|
||||
intro a H',
|
||||
exact H a (mem_insert_of_mem a' H')
|
||||
end
|
||||
|
||||
proposition Max_add_right (f : A → B) {s : finset A} (b : B) (sne : s ≠ ∅) :
|
||||
(Max x ∈ s, f x + b) = (Max x ∈ s, f x) + b :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'ne,
|
||||
{rewrite [s'empty, Max_singleton]},
|
||||
rewrite [*Max_insert _ a'nins' s'ne, ih s'ne, max_add_add_right]
|
||||
end
|
||||
|
||||
proposition Max_add_left (f : A → B) {s : finset A} (b : B) (sne : s ≠ ∅) :
|
||||
(Max x ∈ s, b + f x) = b + (Max x ∈ s, f x) :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'ne,
|
||||
{rewrite [s'empty, Max_singleton]},
|
||||
rewrite [*Max_insert _ a'nins' s'ne, ih s'ne, max_add_add_left]
|
||||
end
|
||||
|
||||
section min_comm_semigroup
|
||||
local attribute min_comm_semigroup [instance]
|
||||
open Prod_semigroup
|
||||
|
||||
definition Min (s : finset A) (f : A → B) : B := Prod_semigroup 0 s f
|
||||
notation `Min` binders `∈` s `, ` r:(scoped f, Min s f) := r
|
||||
|
||||
proposition Min_empty (f : A → B) : (Min x ∈ ∅, f x) = 0 := !Prod_semigroup_empty
|
||||
|
||||
proposition Min_singleton (f : A → B) (a : A) : (Min x ∈ '{a}, f x) = f a :=
|
||||
!Prod_semigroup_singleton
|
||||
|
||||
proposition Min_insert_insert (f : A → B) {a₁ a₂ : A} {s : finset A} :
|
||||
a₂ ∉ s → a₁ ∉ insert a₂ s →
|
||||
(Min x ∈ insert a₁ (insert a₂ s), f x) = min (f a₁) (Min x ∈ insert a₂ s, f x) :=
|
||||
!Prod_semigroup_insert_insert
|
||||
|
||||
proposition Min_insert (f : A → B) {a : A} {s : finset A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
(Min x ∈ insert a s, f x) = min (f a) (Min x ∈ s, f x) :=
|
||||
!Prod_semigroup_insert anins sne
|
||||
end min_comm_semigroup
|
||||
|
||||
proposition Min_pair (f : A → B) (a₁ a₂ : A) : (Min x ∈ '{a₁, a₂}, f x) = min (f a₁) (f a₂) :=
|
||||
decidable.by_cases
|
||||
(suppose a₁ = a₂, by rewrite [this, pair_eq_singleton, min_self] )
|
||||
(suppose a₁ ≠ a₂,
|
||||
have a₁ ∉ '{a₂}, by rewrite [mem_singleton_iff]; apply this,
|
||||
using this, by rewrite [Min_insert f this !singleton_ne_empty])
|
||||
|
||||
proposition Min_le (f : A → B) {a : A} {s : finset A} (H : a ∈ s) : (Min x ∈ s, f x) ≤ f a :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact false.elim (not_mem_empty a H)},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'nempty,
|
||||
{rewrite [s'empty at *, Min_singleton, eq_of_mem_singleton H], apply le.refl},
|
||||
rewrite [Min_insert f a'nins' s'nempty],
|
||||
cases (eq_or_mem_of_mem_insert H) with aeqa' ains',
|
||||
{rewrite aeqa', apply min_le_left},
|
||||
apply le.trans !min_le_right (ih ains')
|
||||
end
|
||||
|
||||
proposition le_Min (f : A → B) {s : finset A} {b : B} (sne : s ≠ ∅) (H : ∀ a, a ∈ s → b ≤ f a) :
|
||||
b ≤ Min x ∈ s, f x :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'nempty,
|
||||
{rewrite [s'empty, Min_singleton], exact H a' !mem_insert},
|
||||
rewrite [Min_insert f a'nins' s'nempty],
|
||||
apply le_min (H a' !mem_insert),
|
||||
apply ih s'nempty,
|
||||
intro a H',
|
||||
exact H a (mem_insert_of_mem a' H')
|
||||
end
|
||||
|
||||
proposition Min_add_right (f : A → B) {s : finset A} (b : B) (sne : s ≠ ∅) :
|
||||
(Min x ∈ s, f x + b) = (Min x ∈ s, f x) + b :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'ne,
|
||||
{rewrite [s'empty, Min_singleton]},
|
||||
rewrite [*Min_insert _ a'nins' s'ne, ih s'ne, min_add_add_right]
|
||||
end
|
||||
|
||||
proposition Min_add_left (f : A → B) {s : finset A} (b : B) (sne : s ≠ ∅) :
|
||||
(Min x ∈ s, b + f x) = b + (Min x ∈ s, f x) :=
|
||||
begin
|
||||
induction s with a' s' a'nins' ih,
|
||||
{exact absurd rfl sne},
|
||||
cases (decidable.em (s' = ∅)) with s'empty s'ne,
|
||||
{rewrite [s'empty, Min_singleton]},
|
||||
rewrite [*Min_insert _ a'nins' s'ne, ih s'ne, min_add_add_left]
|
||||
end
|
||||
end decidable_linear_ordered_cancel_comm_monoid_B
|
||||
|
||||
section decidable_linear_ordered_comm_group_B
|
||||
variable [decidable_linear_ordered_comm_group B]
|
||||
|
||||
proposition Max_neg (f : A → B) (s : finset A) : (Max x ∈ s, - f x) = - Min x ∈ s, f x :=
|
||||
begin
|
||||
cases (decidable.em (s = ∅)) with se sne,
|
||||
{rewrite [se, Max_empty, Min_empty, neg_zero]},
|
||||
apply eq_of_le_of_ge,
|
||||
{apply !Max_le sne,
|
||||
intro a ains,
|
||||
apply neg_le_neg,
|
||||
apply !Min_le ains},
|
||||
apply neg_le_of_neg_le,
|
||||
apply !le_Min sne,
|
||||
intro a ains,
|
||||
apply neg_le_of_neg_le,
|
||||
apply !le_Max ains
|
||||
end
|
||||
|
||||
proposition Min_neg (f : A → B) (s : finset A) : (Min x ∈ s, - f x) = - Max x ∈ s, f x :=
|
||||
begin
|
||||
cases (decidable.em (s = ∅)) with se sne,
|
||||
{rewrite [se, Max_empty, Min_empty, neg_zero]},
|
||||
apply eq_of_le_of_ge,
|
||||
{apply le_neg_of_le_neg,
|
||||
apply !Max_le sne,
|
||||
intro a ains,
|
||||
apply le_neg_of_le_neg,
|
||||
apply !Min_le ains},
|
||||
apply !le_Min sne,
|
||||
intro a ains,
|
||||
apply neg_le_neg,
|
||||
apply !le_Max ains
|
||||
end
|
||||
|
||||
proposition Max_eq_neg_Min_neg (f : A → B) (s : finset A) :
|
||||
(Max x ∈ s, f x) = - Min x ∈ s, - f x :=
|
||||
by rewrite [Min_neg, neg_neg]
|
||||
|
||||
proposition Min_eq_neg_Max_neg (f : A → B) (s : finset A) :
|
||||
(Min x ∈ s, f x) = - Max x ∈ s, - f x :=
|
||||
by rewrite [Max_neg, neg_neg]
|
||||
|
||||
end decidable_linear_ordered_comm_group_B
|
||||
|
||||
end deceq_A
|
||||
|
||||
/- Min and Max *of* a finset -/
|
||||
|
||||
section decidable_linear_ordered_semiring_A
|
||||
variable [decidable_linear_ordered_semiring A]
|
||||
|
||||
definition Max₀ (s : finset A) : A := Max x ∈ s, x
|
||||
definition Min₀ (s : finset A) : A := Min x ∈ s, x
|
||||
|
||||
proposition Max₀_empty : Max₀ ∅ = (0 : A) := !Max_empty
|
||||
|
||||
proposition Max₀_singleton (a : A) : Max₀ '{a} = a := !Max_singleton
|
||||
|
||||
proposition Max₀_insert_insert {a₁ a₂ : A} {s : finset A} (H₁ : a₂ ∉ s) (H₂ : a₁ ∉ insert a₂ s) :
|
||||
Max₀ (insert a₁ (insert a₂ s)) = max a₁ (Max₀ (insert a₂ s)) :=
|
||||
!Max_insert_insert H₁ H₂
|
||||
|
||||
proposition Max₀_insert {s : finset A} {a : A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
Max₀ (insert a s) = max a (Max₀ s) := !Max_insert anins sne
|
||||
|
||||
proposition Max₀_pair (a₁ a₂ : A) : Max₀ '{a₁, a₂} = max a₁ a₂ := !Max_pair
|
||||
|
||||
proposition le_Max₀ {a : A} {s : finset A} (H : a ∈ s) : a ≤ Max₀ s := !le_Max H
|
||||
|
||||
proposition Max₀_le {s : finset A} {a : A} (sne : s ≠ ∅) (H : ∀ x, x ∈ s → x ≤ a) :
|
||||
Max₀ s ≤ a := !Max_le sne H
|
||||
|
||||
proposition Min₀_empty : Min₀ ∅ = (0 : A) := !Min_empty
|
||||
|
||||
proposition Min₀_singleton (a : A) : Min₀ '{a} = a := !Min_singleton
|
||||
|
||||
proposition Min₀_insert_insert {a₁ a₂ : A} {s : finset A} (H₁ : a₂ ∉ s) (H₂ : a₁ ∉ insert a₂ s) :
|
||||
Min₀ (insert a₁ (insert a₂ s)) = min a₁ (Min₀ (insert a₂ s)) :=
|
||||
!Min_insert_insert H₁ H₂
|
||||
|
||||
proposition Min₀_insert {s : finset A} {a : A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
Min₀ (insert a s) = min a (Min₀ s) := !Min_insert anins sne
|
||||
|
||||
proposition Min₀_pair (a₁ a₂ : A) : Min₀ '{a₁, a₂} = min a₁ a₂ := !Min_pair
|
||||
|
||||
proposition Min₀_le {a : A} {s : finset A} (H : a ∈ s) : Min₀ s ≤ a := !Min_le H
|
||||
|
||||
proposition le_Min₀ {s : finset A} {a : A} (sne : s ≠ ∅) (H : ∀ x, x ∈ s → a ≤ x) :
|
||||
a ≤ Min₀ s := !le_Min sne H
|
||||
end decidable_linear_ordered_semiring_A
|
||||
|
||||
end finset
|
||||
|
||||
/- finite set versions -/
|
||||
|
||||
namespace set
|
||||
open classical
|
||||
|
||||
section decidable_linear_ordered_cancel_comm_monoid_B
|
||||
variable [decidable_linear_ordered_cancel_comm_monoid B]
|
||||
|
||||
noncomputable definition Max (s : set A) (f : A → B) : B := finset.Max (to_finset s) f
|
||||
notation `Max` binders `∈` s `, ` r:(scoped f, Max s f) := r
|
||||
|
||||
noncomputable definition Min (s : set A) (f : A → B) : B := finset.Min (to_finset s) f
|
||||
notation `Min` binders `∈` s `, ` r:(scoped f, Min s f) := r
|
||||
|
||||
proposition Max_empty (f : A → B) : (Max x ∈ ∅, f x) = 0 :=
|
||||
by rewrite [↑set.Max, to_finset_empty, finset.Max_empty]
|
||||
|
||||
proposition Max_singleton (f : A → B) (a : A) : (Max x ∈ '{a}, f x) = f a :=
|
||||
by rewrite [↑set.Max, to_finset_insert, to_finset_empty, finset.Max_singleton]
|
||||
|
||||
proposition Max_insert_insert (f : A → B) {a₁ a₂ : A} {s : set A} [h : finite s] :
|
||||
a₂ ∉ s → a₁ ∉ insert a₂ s →
|
||||
(Max x ∈ insert a₁ (insert a₂ s), f x) = max (f a₁) (Max x ∈ insert a₂ s, f x) :=
|
||||
begin
|
||||
rewrite [↑set.Max, -+mem_to_finset_eq, +to_finset_insert],
|
||||
apply finset.Max_insert_insert
|
||||
end
|
||||
|
||||
proposition Max_insert (f : A → B) {a : A} {s : set A} [h : finite s] (anins : a ∉ s)
|
||||
(sne : s ≠ ∅) :
|
||||
(Max x ∈ insert a s, f x) = max (f a) (Max x ∈ s, f x) :=
|
||||
begin
|
||||
revert anins sne,
|
||||
rewrite [↑set.Max, -+mem_to_finset_eq, +to_finset_insert],
|
||||
intro h1 h2,
|
||||
apply finset.Max_insert f h1 (λ h', h2 (eq_empty_of_to_finset_eq_empty h')),
|
||||
end
|
||||
|
||||
proposition Max_pair (f : A → B) (a₁ a₂ : A) : (Max x ∈ '{a₁, a₂}, f x) = max (f a₁) (f a₂) :=
|
||||
by rewrite [↑set.Max, +to_finset_insert, +to_finset_empty, finset.Max_pair]
|
||||
|
||||
proposition le_Max (f : A → B) {a : A} {s : set A} [fins : finite s] (H : a ∈ s) :
|
||||
f a ≤ Max x ∈ s, f x :=
|
||||
by rewrite [-+mem_to_finset_eq at H, ↑set.Max]; exact finset.le_Max f H
|
||||
|
||||
proposition Max_le (f : A → B) {s : set A} [fins : finite s] {b : B} (sne : s ≠ ∅)
|
||||
(H : ∀ a, a ∈ s → f a ≤ b) :
|
||||
(Max x ∈ s, f x) ≤ b :=
|
||||
begin
|
||||
rewrite [↑set.Max],
|
||||
apply finset.Max_le f (λ H', sne (eq_empty_of_to_finset_eq_empty H')),
|
||||
intro a H', apply H a, rewrite mem_to_finset_eq at H', exact H'
|
||||
end
|
||||
|
||||
proposition Max_add_right (f : A → B) {s : set A} [fins : finite s] (b : B) (sne : s ≠ ∅) :
|
||||
(Max x ∈ s, f x + b) = (Max x ∈ s, f x) + b :=
|
||||
begin
|
||||
rewrite [↑set.Max],
|
||||
apply finset.Max_add_right f b (λ h, sne (eq_empty_of_to_finset_eq_empty h))
|
||||
end
|
||||
|
||||
proposition Max_add_left (f : A → B) {s : set A} [fins : finite s] (b : B) (sne : s ≠ ∅) :
|
||||
(Max x ∈ s, b + f x) = b + (Max x ∈ s, f x) :=
|
||||
begin
|
||||
rewrite [↑set.Max],
|
||||
apply finset.Max_add_left f b (λ h, sne (eq_empty_of_to_finset_eq_empty h))
|
||||
end
|
||||
|
||||
proposition Min_empty (f : A → B) : (Min x ∈ ∅, f x) = 0 :=
|
||||
by rewrite [↑set.Min, to_finset_empty, finset.Min_empty]
|
||||
|
||||
proposition Min_singleton (f : A → B) (a : A) : (Min x ∈ '{a}, f x) = f a :=
|
||||
by rewrite [↑set.Min, to_finset_insert, to_finset_empty, finset.Min_singleton]
|
||||
|
||||
proposition Min_insert_insert (f : A → B) {a₁ a₂ : A} {s : set A} [h : finite s] :
|
||||
a₂ ∉ s → a₁ ∉ insert a₂ s →
|
||||
(Min x ∈ insert a₁ (insert a₂ s), f x) = min (f a₁) (Min x ∈ insert a₂ s, f x) :=
|
||||
begin
|
||||
rewrite [↑set.Min, -+mem_to_finset_eq, +to_finset_insert],
|
||||
apply finset.Min_insert_insert
|
||||
end
|
||||
|
||||
proposition Min_insert (f : A → B) {a : A} {s : set A} [h : finite s] (anins : a ∉ s)
|
||||
(sne : s ≠ ∅) :
|
||||
(Min x ∈ insert a s, f x) = min (f a) (Min x ∈ s, f x) :=
|
||||
begin
|
||||
revert anins sne,
|
||||
rewrite [↑set.Min, -+mem_to_finset_eq, +to_finset_insert],
|
||||
intro h1 h2,
|
||||
apply finset.Min_insert f h1 (λ h', h2 (eq_empty_of_to_finset_eq_empty h')),
|
||||
end
|
||||
|
||||
proposition Min_pair (f : A → B) (a₁ a₂ : A) : (Min x ∈ '{a₁, a₂}, f x) = min (f a₁) (f a₂) :=
|
||||
by rewrite [↑set.Min, +to_finset_insert, +to_finset_empty, finset.Min_pair]
|
||||
|
||||
proposition Min_le (f : A → B) {a : A} {s : set A} [fins : finite s] (H : a ∈ s) :
|
||||
(Min x ∈ s, f x) ≤ f a :=
|
||||
by rewrite [-+mem_to_finset_eq at H, ↑set.Min]; exact finset.Min_le f H
|
||||
|
||||
proposition le_Min (f : A → B) {s : set A} [fins : finite s] {b : B} (sne : s ≠ ∅)
|
||||
(H : ∀ a, a ∈ s → b ≤ f a) :
|
||||
b ≤ Min x ∈ s, f x :=
|
||||
begin
|
||||
rewrite [↑set.Min],
|
||||
apply finset.le_Min f (λ H', sne (eq_empty_of_to_finset_eq_empty H')),
|
||||
intro a H', apply H a, rewrite mem_to_finset_eq at H', exact H'
|
||||
end
|
||||
|
||||
proposition Min_add_right (f : A → B) {s : set A} [fins : finite s] (b : B) (sne : s ≠ ∅) :
|
||||
(Min x ∈ s, f x + b) = (Min x ∈ s, f x) + b :=
|
||||
begin
|
||||
rewrite [↑set.Min],
|
||||
apply finset.Min_add_right f b (λ h, sne (eq_empty_of_to_finset_eq_empty h))
|
||||
end
|
||||
|
||||
proposition Min_add_left (f : A → B) {s : set A} [fins : finite s] (b : B) (sne : s ≠ ∅) :
|
||||
(Min x ∈ s, b + f x) = b + (Min x ∈ s, f x) :=
|
||||
begin
|
||||
rewrite [↑set.Min],
|
||||
apply finset.Min_add_left f b (λ h, sne (eq_empty_of_to_finset_eq_empty h))
|
||||
end
|
||||
end decidable_linear_ordered_cancel_comm_monoid_B
|
||||
|
||||
section decidable_linear_ordered_comm_group_B
|
||||
variable [decidable_linear_ordered_comm_group B]
|
||||
|
||||
proposition Max_neg (f : A → B) (s : set A) : (Max x ∈ s, - f x) = - Min x ∈ s, f x :=
|
||||
by rewrite [↑set.Max, finset.Max_neg]
|
||||
|
||||
proposition Min_neg (f : A → B) (s : set A) : (Min x ∈ s, - f x) = - Max x ∈ s, f x :=
|
||||
by rewrite [↑set.Min, finset.Min_neg]
|
||||
|
||||
proposition Max_eq_neg_Min_neg (f : A → B) (s : set A) : (Max x ∈ s, f x) = - Min x ∈ s, - f x :=
|
||||
by rewrite [↑set.Max, ↑set.Min, finset.Max_eq_neg_Min_neg]
|
||||
|
||||
proposition Min_eq_neg_Max_neg (f : A → B) (s : set A) : (Min x ∈ s, f x) = - Max x ∈ s, - f x :=
|
||||
by rewrite [↑set.Max, ↑set.Min, finset.Min_eq_neg_Max_neg]
|
||||
end decidable_linear_ordered_comm_group_B
|
||||
|
||||
section decidable_linear_ordered_semiring_A
|
||||
variable [decidable_linear_ordered_semiring A]
|
||||
|
||||
noncomputable definition Max₀ (s : set A) : A := Max x ∈ s, x
|
||||
noncomputable definition Min₀ (s : set A) : A := Min x ∈ s, x
|
||||
|
||||
proposition Max₀_empty : Max₀ ∅ = (0 : A) := !Max_empty
|
||||
|
||||
proposition Max₀_singleton (a : A) : Max₀ '{a} = a := !Max_singleton
|
||||
|
||||
proposition Max₀_insert_insert {a₁ a₂ : A} {s : set A} [fins : finite s] (H₁ : a₂ ∉ s)
|
||||
(H₂ : a₁ ∉ insert a₂ s) :
|
||||
Max₀ (insert a₁ (insert a₂ s)) = max a₁ (Max₀ (insert a₂ s)) :=
|
||||
!Max_insert_insert H₁ H₂
|
||||
|
||||
proposition Max₀_insert {s : set A} [fins : finite s] {a : A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
Max₀ (insert a s) = max a (Max₀ s) := !Max_insert anins sne
|
||||
|
||||
proposition Max₀_pair (a₁ a₂ : A) : Max₀ '{a₁, a₂} = max a₁ a₂ := !Max_pair
|
||||
|
||||
proposition le_Max₀ {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : a ≤ Max₀ s := !le_Max H
|
||||
|
||||
proposition Max₀_le {s : set A} [fins : finite s] {a : A} (sne : s ≠ ∅) (H : ∀ x, x ∈ s → x ≤ a) :
|
||||
Max₀ s ≤ a := !Max_le sne H
|
||||
|
||||
proposition Min₀_empty : Min₀ ∅ = (0 : A) := !Min_empty
|
||||
|
||||
proposition Min₀_singleton (a : A) : Min₀ '{a} = a := !Min_singleton
|
||||
|
||||
proposition Min₀_insert_insert {a₁ a₂ : A} {s : set A} [fins : finite s] (H₁ : a₂ ∉ s)
|
||||
(H₂ : a₁ ∉ insert a₂ s) :
|
||||
Min₀ (insert a₁ (insert a₂ s)) = min a₁ (Min₀ (insert a₂ s)) :=
|
||||
!Min_insert_insert H₁ H₂
|
||||
|
||||
proposition Min₀_insert {s : set A} [fins : finite s] {a : A} (anins : a ∉ s) (sne : s ≠ ∅) :
|
||||
Min₀ (insert a s) = min a (Min₀ s) := !Min_insert anins sne
|
||||
|
||||
proposition Min₀_pair (a₁ a₂ : A) : Min₀ '{a₁, a₂} = min a₁ a₂ := !Min_pair
|
||||
|
||||
proposition Min₀_le {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : Min₀ s ≤ a := !Min_le H
|
||||
|
||||
proposition le_Min₀ {s : set A} [fins : finite s] {a : A} (sne : s ≠ ∅) (H : ∀ x, x ∈ s → a ≤ x) :
|
||||
a ≤ Min₀ s := !le_Min sne H
|
||||
end decidable_linear_ordered_semiring_A
|
||||
|
||||
end set
|
||||
Loading…
Add table
Reference in a new issue