michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/algebra/monotone): add properties of monotone functions

Browse source
This commit is contained in:
Jeremy Avigad 2016-02-28 21:55:48 -05:00
parent 3d09144d73
commit ebb3e60096
9 changed files with 691 additions and 120 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/algebra/algebra.md
View file

@ -24,5 +24,6 @@ Algebraic 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
* [monotone](monotone.lean) : monotone maps between order structures
* [homomorphism](homomorphism.lean) : homomorphisms between algebraic structures
* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)

15
library/algebra/complete_lattice.lean
View file

@ -7,7 +7,7 @@ Complete lattices
TODO: define dual complete lattice and simplify proof of dual theorems.
-/
import algebra.lattice data.set.basic
import algebra.lattice data.set.basic algebra.monotone
open set
variable {A : Type}
@ -109,7 +109,8 @@ Sup_le (take x, suppose x ∈ '{a, b},
end complete_lattice_Inf
-- Every complete_lattice_Inf is a complete_lattice_Sup
definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_Inf A] : complete_lattice_Sup A :=
definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_Inf A] :
complete_lattice_Sup A :=
⦃ complete_lattice_Sup, C ⦄
-- Every complete_lattice_Inf is a complete_lattice
@ -172,9 +173,9 @@ Sup_le (take x, suppose x ∈ '{a, b},
end complete_lattice_Sup
-- Every complete_lattice_Sup is a complete_lattice_Inf
definition complete_lattice_Sup_to_complete_lattice_Inf [C : complete_lattice_Sup A] : complete_lattice_Inf A :=
definition complete_lattice_Sup_to_complete_lattice_Inf [C : complete_lattice_Sup A] :
complete_lattice_Inf A :=
⦃ complete_lattice_Inf, C ⦄
-- Every complete_lattice_Sup is a complete_lattice
@ -189,7 +190,7 @@ variable [C : complete_lattice A]
include C
variable {f : A → A}
premise (mono : ∀ x y : A, x ≤ y → f x ≤ f y)
premise (mono : nondecreasing f)
theorem knaster_tarski : ∃ a, f a = a ∧ ∀ b, f b = b → a ≤ b :=
let a := ⨅ {u | f u ≤ u} in
@ -198,7 +199,7 @@ have h₁ : f a = a, from
have ∀ b, b ∈ {u | f u ≤ u} → f a ≤ b, from
take b, suppose f b ≤ b,
have a ≤ b, from Inf_le this,
have f a ≤ f b, from !mono this,
have f a ≤ f b, from mono this,
le.trans `f a ≤ f b` `f b ≤ b`,
le_Inf this,
have le : a ≤ f a, from
@ -221,7 +222,7 @@ have h₁ : f a = a, from
have ∀ b, b ∈ {u | u ≤ f u} → b ≤ f a, from
take b, suppose b ≤ f b,
have b ≤ a, from le_Sup this,
have f b ≤ f a, from !mono this,
have f b ≤ f a, from mono this,
le.trans `b ≤ f b` `f b ≤ f a`,
Sup_le this,
have ge : f a ≤ a, from

26
library/algebra/group.lean
View file

@ -165,6 +165,11 @@ section group
theorem inv_inv [simp] (a : A) : (a⁻¹)⁻¹ = a :=
inv_eq_of_mul_eq_one (mul.left_inv a)
variable (A)
theorem left_inverse_inv : function.left_inverse (λ a : A, a⁻¹) (λ a, a⁻¹) :=
take a, inv_inv a
variable {A}
theorem inv.inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
have a = a⁻¹⁻¹, by simp_nohyps,
by inst_simp
@ -331,6 +336,11 @@ section add_group
theorem neg_neg [simp] (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
variable (A)
theorem left_inverse_neg : function.left_inverse (λ a : A, - a) (λ a, - a) :=
take a, neg_neg a
variable {A}
theorem eq_neg_of_add_eq_zero {a b : A} (H : a + b = 0) : a = -b :=
have -a = b, from neg_eq_of_add_eq_zero H,
by inst_simp
@ -414,7 +424,8 @@ section add_group
⦃ add_left_cancel_semigroup, s,
add_left_cancel := @add_left_cancel A s ⦄
definition add_group.to_add_right_cancel_semigroup [trans_instance] : add_right_cancel_semigroup A :=
definition add_group.to_add_right_cancel_semigroup [trans_instance] :
add_right_cancel_semigroup A :=
⦃ add_right_cancel_semigroup, s,
add_right_cancel := @add_right_cancel A s ⦄
@ -513,6 +524,19 @@ section add_group
theorem add_eq_of_eq_sub {a b c : A} (H : a = c - b) : a + b = c :=
by simp
theorem left_inverse_sub_add_left (c : A) : function.left_inverse (λ x, x - c) (λ x, x + c) :=
take x, add_sub_cancel x c
theorem left_inverse_add_left_sub (c : A) : function.left_inverse (λ x, x + c) (λ x, x - c) :=
take x, sub_add_cancel x c
theorem left_inverse_add_right_neg_add (c : A) :
function.left_inverse (λ x, c + x) (λ x, - c + x) :=
take x, add_neg_cancel_left c x
theorem left_inverse_neg_add_add_right (c : A) :
function.left_inverse (λ x, - c + x) (λ x, c + x) :=
take x, neg_add_cancel_left c x
end add_group
structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A

4
library/algebra/homomorphism.lean
View file

@ -73,7 +73,7 @@ section add_group_A_B
injective f :=
take x₁ x₂,
suppose f x₁ = f x₂,
have f (x₁ - x₂) = 0, using this, by rewrite [hom_sub, this, sub_self],
have f (x₁ - x₂) = 0, by rewrite [hom_sub, this, sub_self],
have x₁ - x₂ = 0, from H _ this,
eq_of_sub_eq_zero this
@ -124,7 +124,7 @@ section group_A_B
injective f :=
take x₁ x₂,
suppose f x₁ = f x₂,
have f (x₁ * x₂⁻¹) = 1, using this, by rewrite [hom_mul, hom_inv, this, mul.right_inv],
have f (x₁ * x₂⁻¹) = 1, by rewrite [hom_mul, hom_inv, this, mul.right_inv],
have x₁ * x₂⁻¹ = 1, from H _ this,
eq_of_mul_inv_eq_one this

418
library/algebra/monotone.lean Normal file
View file

@ -0,0 +1,418 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Weak and strict order preserving maps.
TODO: we will probably eventually want versions restricted to smaller domains,
"nondecreasing_on" etc. Maybe we can do this with subtypes.
-/
import .order
open eq eq.ops function
variables {A B C : Type}
section
variables [weak_order A] [weak_order B] [weak_order C]
definition nondecreasing (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, a₁ ≤ a₂ → f a₁ ≤ f a₂
definition nonincreasing (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, a₁ ≤ a₂ → f a₁ ≥ f a₂
theorem nondecreasing_id : nondecreasing (@id A) := take a₁ a₂, assume H, H
theorem nondecreasing_comp_nondec_nondec {g : B → C} {f : A → B}
(Hg : nondecreasing g) (Hf : nondecreasing f) : nondecreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem nondecreasing_comp_noninc_noninc {g : B → C} {f : A → B}
(Hg : nonincreasing g) (Hf : nonincreasing f) : nondecreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem nonincreasing_comp_noninc_nondec {g : B → C} {f : A → B}
(Hg : nonincreasing g) (Hf : nondecreasing f) : nonincreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem nonincreasing_comp_nondec_noninc {g : B → C} {f : A → B}
(Hg : nondecreasing g) (Hf : nonincreasing f) : nonincreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
end
section
variables [strict_order A] [strict_order B] [strict_order C]
definition strictly_increasing (f : A → B) : Prop :=
∀ ⦃a₁ a₂⦄, a₁ < a₂ → f a₁ < f a₂
definition strictly_decreasing (f : A → B) : Prop :=
∀ ⦃a₁ a₂⦄, a₁ < a₂ → f a₁ > f a₂
theorem strictly_increasing_id : strictly_increasing (@id A) := take a₁ a₂, assume H, H
theorem strictly_increasing_comp_inc_inc {g : B → C} {f : A → B}
(Hg : strictly_increasing g) (Hf : strictly_increasing f) : strictly_increasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem strictly_increasing_comp_dec_dec {g : B → C} {f : A → B}
(Hg : strictly_decreasing g) (Hf : strictly_decreasing f) : strictly_increasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem strictly_decreasing_comp_inc_dec {g : B → C} {f : A → B}
(Hg : strictly_increasing g) (Hf : strictly_decreasing f) : strictly_decreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
theorem strictly_decreasing_comp_dec_inc {g : B → C} {f : A → B}
(Hg : strictly_decreasing g) (Hf : strictly_increasing f) : strictly_decreasing (g ∘ f) :=
take a₁ a₂, assume H, Hg (Hf H)
end
section
variables [strong_order_pair A] [strong_order_pair B]
theorem nondecreasing_of_strictly_increasing {f : A → B} (H : strictly_increasing f) :
nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
show f a₁ ≤ f a₂, from or.elim (lt_or_eq_of_le this)
(suppose a₁ < a₂, le_of_lt (H this))
(suppose a₁ = a₂, le_of_eq (congr_arg f this))
theorem nonincreasing_of_strictly_decreasing {f : A → B} (H : strictly_decreasing f) :
nonincreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
show f a₁ ≥ f a₂, from or.elim (lt_or_eq_of_le this)
(suppose a₁ < a₂, le_of_lt (H this))
(suppose a₁ = a₂, le_of_eq (congr_arg f this⁻¹))
end
section
variables [linear_strong_order_pair A] [linear_strong_order_pair B] [linear_strong_order_pair C]
theorem lt_of_strictly_increasing {f : A → B} {a₁ a₂ : A} (H : strictly_increasing f)
(H' : f a₁ < f a₂) : a₁ < a₂ :=
lt_of_not_ge (suppose a₂ ≤ a₁,
have f a₂ ≤ f a₁, from nondecreasing_of_strictly_increasing H this,
show false, from not_le_of_gt H' this)
theorem lt_iff_of_strictly_increasing {f : A → B} (a₁ a₂ : A) (H : strictly_increasing f) :
f a₁ < f a₂ ↔ a₁ < a₂ :=
iff.intro (lt_of_strictly_increasing H) (@H a₁ a₂)
theorem le_of_strictly_increasing {f : A → B} {a₁ a₂ : A} (H : strictly_increasing f)
(H' : f a₁ ≤ f a₂) : a₁ ≤ a₂ :=
le_of_not_gt (suppose a₂ < a₁, not_le_of_gt (H this) H')
theorem le_iff_of_strictly_increasing {f : A → B} (a₁ a₂ : A) (H : strictly_increasing f) :
f a₁ ≤ f a₂ ↔ a₁ ≤ a₂ :=
iff.intro (le_of_strictly_increasing H) (λ H', nondecreasing_of_strictly_increasing H H')
theorem lt_of_strictly_decreasing {f : A → B} {a₁ a₂ : A} (H : strictly_decreasing f)
(H' : f a₁ > f a₂) : a₁ < a₂ :=
lt_of_not_ge (suppose a₂ ≤ a₁,
have f a₂ ≥ f a₁, from nonincreasing_of_strictly_decreasing H this,
show false, from not_le_of_gt H' this)
theorem gt_iff_of_strictly_decreasing {f : A → B} (a₁ a₂ : A) (H : strictly_decreasing f) :
f a₁ > f a₂ ↔ a₁ < a₂ :=
iff.intro (lt_of_strictly_decreasing H) (@H a₁ a₂)
theorem le_of_strictly_decreasing {f : A → B} {a₁ a₂ : A} (H : strictly_decreasing f)
(H' : f a₁ ≥ f a₂) : a₁ ≤ a₂ :=
le_of_not_gt (suppose a₂ < a₁, not_le_of_gt (H this) H')
theorem ge_iff_of_strictly_decreasing {f : A → B} (a₁ a₂ : A) (H : strictly_decreasing f) :
f a₁ ≥ f a₂ ↔ a₁ ≤ a₂ :=
iff.intro (le_of_strictly_decreasing H) (λ H', nonincreasing_of_strictly_decreasing H H')
theorem strictly_increasing_of_left_inverse {g : B → A} {f : A → B} (H : left_inverse g f)
(H' : strictly_increasing g) : strictly_increasing f :=
take a₁ a₂, suppose a₁ < a₂,
have g (f a₁) < g (f a₂), by rewrite *H; apply this,
lt_of_strictly_increasing H' this
theorem strictly_decreasing_of_left_inverse {g : B → A} {f : A → B} (H : left_inverse g f)
(H' : strictly_decreasing g) : strictly_decreasing f :=
take b₁ b₂, suppose b₁ < b₂,
have g (f b₁) < g (f b₂), by rewrite *H; apply this,
lt_of_strictly_decreasing H' this
theorem nondecreasing_of_left_inverse {g : B → A} {f : A → B} (H : left_inverse g f)
(H' : strictly_increasing g) : nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have g (f a₁) ≤ g (f a₂), by rewrite *H; apply this,
le_of_strictly_increasing H' this
theorem nonincreasing_of_left_inverse {g : B → A} {f : A → B} (H : left_inverse g f)
(H' : strictly_decreasing g) : nonincreasing f :=
take b₁ b₂, suppose b₁ ≤ b₂,
have g (f b₁) ≤ g (f b₂), by rewrite *H; apply this,
le_of_strictly_decreasing H' this
end
/- composition rules for strict orders -/
section
variables [strict_order A] [strict_order B] [strict_order C]
theorem strictly_increasing_of_strictly_increasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) (H₃ : strictly_increasing (g ∘ f)) :
strictly_increasing f :=
take a₁ a₂, suppose a₁ < a₂,
have h (g (f a₁)) < h (g (f a₂)), from H₂ (H₃ this),
show f a₁ < f a₂, by rewrite *H₁ at this; apply this
theorem strictly_decreasing_of_strictly_increasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) (H₃ : strictly_increasing (g ∘ f)) :
strictly_decreasing f :=
take a₁ a₂, suppose a₁ < a₂,
have h (g (f a₁)) > h (g (f a₂)), from H₂ (H₃ this),
show f a₁ > f a₂, by rewrite *H₁ at this; apply this
theorem strictly_decreasing_of_strictly_decreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) (H₃ : strictly_decreasing (g ∘ f)) :
strictly_decreasing f :=
take a₁ a₂, suppose a₁ < a₂,
have h (g (f a₁)) > h (g (f a₂)), from H₂ (H₃ this),
show f a₁ > f a₂, by rewrite *H₁ at this; apply this
theorem strictly_increasing_of_strictly_decreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) (H₃ : strictly_decreasing (g ∘ f)) :
strictly_increasing f :=
take a₁ a₂, suppose a₁ < a₂,
have h (g (f a₁)) < h (g (f a₂)), from H₂ (H₃ this),
show f a₁ < f a₂, by rewrite *H₁ at this; apply this
theorem strictly_increasing_of_strictly_decreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing h) (H₃ : strictly_decreasing (g ∘ f)) :
strictly_increasing g :=
take a₁ a₂, suppose a₁ < a₂,
have g (f (h a₁)) < g (f (h a₂)), from H₃ (H₂ this),
show g a₁ < g a₂, by rewrite *H₁ at this; apply this
theorem strictly_decreasing_of_strictly_decreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing h) (H₃ : strictly_decreasing (g ∘ f)) :
strictly_decreasing g :=
take a₁ a₂, suppose a₁ < a₂,
have g (f (h a₁)) > g (f (h a₂)), from H₃ (H₂ this),
show g a₁ > g a₂, by rewrite *H₁ at this; apply this
theorem strictly_increasing_of_strictly_increasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing h) (H₃ : strictly_increasing (g ∘ f)) :
strictly_increasing g :=
take a₁ a₂, suppose a₁ < a₂,
have g (f (h a₁)) < g (f (h a₂)), from H₃ (H₂ this),
show g a₁ < g a₂, by rewrite *H₁ at this; apply this
theorem strictly_decreasing_of_strictly_increasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing h) (H₃ : strictly_increasing (g ∘ f)) :
strictly_decreasing g :=
take a₁ a₂, suppose a₁ < a₂,
have g (f (h a₁)) > g (f (h a₂)), from H₃ (H₂ this),
show g a₁ > g a₂, by rewrite *H₁ at this; apply this
end
section
variables [strict_order A] [linear_strong_order_pair B] [linear_strong_order_pair C]
theorem strictly_increasing_comp_iff_strictly_increasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) :
strictly_increasing (g ∘ f) ↔ strictly_increasing f :=
have H₃ : strictly_increasing g, from strictly_increasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_increasing_of_strictly_increasing_comp_right H₁ H₂)
(strictly_increasing_comp_inc_inc H₃)
theorem strictly_increasing_comp_iff_strictly_decreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) :
strictly_increasing (g ∘ f) ↔ strictly_decreasing f :=
have H₃ : strictly_decreasing g, from strictly_decreasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_decreasing_of_strictly_increasing_comp_right H₁ H₂)
(strictly_increasing_comp_dec_dec H₃)
theorem strictly_decreasing_comp_iff_strictly_decreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) :
strictly_decreasing (g ∘ f) ↔ strictly_decreasing f :=
have H₃ : strictly_increasing g, from strictly_increasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_decreasing_of_strictly_decreasing_comp_right H₁ H₂)
(strictly_decreasing_comp_inc_dec H₃)
theorem strictly_decreasing_comp_iff_strictly_increasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) :
strictly_decreasing (g ∘ f) ↔ strictly_increasing f :=
have H₃ : strictly_decreasing g, from strictly_decreasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_increasing_of_strictly_decreasing_comp_right H₁ H₂)
(strictly_decreasing_comp_dec_inc H₃)
end
section
variables [linear_strong_order_pair A] [linear_strong_order_pair B] [strict_order C]
theorem strictly_increasing_comp_iff_strinctly_increasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
strictly_increasing (g ∘ f) ↔ strictly_increasing g :=
have H₃ : strictly_increasing h, from strictly_increasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_increasing_of_strictly_increasing_comp_left H₁ H₃)
(λ H, strictly_increasing_comp_inc_inc H H₂)
theorem strictly_increasing_comp_iff_strictly_decreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
strictly_increasing (g ∘ f) ↔ strictly_decreasing g :=
have H₃ : strictly_decreasing h, from strictly_decreasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_decreasing_of_strictly_increasing_comp_left H₁ H₃)
(λ H, strictly_increasing_comp_dec_dec H H₂)
theorem strictly_decreasing_comp_iff_strictly_increasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
strictly_decreasing (g ∘ f) ↔ strictly_increasing g :=
have H₃ : strictly_decreasing h, from strictly_decreasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_increasing_of_strictly_decreasing_comp_left H₁ H₃)
(λ H, strictly_decreasing_comp_inc_dec H H₂)
theorem strictly_decreasing_comp_iff_strictly_decreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
strictly_decreasing (g ∘ f) ↔ strictly_decreasing g :=
have H₃ : strictly_increasing h, from strictly_increasing_of_left_inverse H₁ H₂,
iff.intro
(strictly_decreasing_of_strictly_decreasing_comp_left H₁ H₃)
(λ H, strictly_decreasing_comp_dec_inc H H₂)
end
/- composition rules for weak orders -/
section
variables [weak_order A] [weak_order B] [weak_order C]
theorem nondecreasing_of_nondecreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : nondecreasing h) (H₃ : nondecreasing (g ∘ f)) :
nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have h (g (f a₁)) ≤ h (g (f a₂)), from H₂ (H₃ this),
show f a₁ ≤ f a₂, by rewrite *H₁ at this; apply this
theorem nonincreasing_of_nondecreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : nonincreasing h) (H₃ : nondecreasing (g ∘ f)) :
nonincreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have h (g (f a₁)) ≥ h (g (f a₂)), from H₂ (H₃ this),
show f a₁ ≥ f a₂, by rewrite *H₁ at this; apply this
theorem nonincreasing_of_nonincreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : nondecreasing h) (H₃ : nonincreasing (g ∘ f)) :
nonincreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have h (g (f a₁)) ≥ h (g (f a₂)), from H₂ (H₃ this),
show f a₁ ≥ f a₂, by rewrite *H₁ at this; apply this
theorem nondecreasing_of_nonincreasing_comp_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : nonincreasing h) (H₃ : nonincreasing (g ∘ f)) :
nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have h (g (f a₁)) ≤ h (g (f a₂)), from H₂ (H₃ this),
show f a₁ ≤ f a₂, by rewrite *H₁ at this; apply this
theorem nondecreasing_of_nondecreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : nondecreasing h) (H₃ : nondecreasing (g ∘ f)) :
nondecreasing g :=
take a₁ a₂, suppose a₁ ≤ a₂,
have g (f (h a₁)) ≤ g (f (h a₂)), from H₃ (H₂ this),
show g a₁ ≤ g a₂, by rewrite *H₁ at this; apply this
theorem nonincreasing_of_nondecreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : nonincreasing h) (H₃ : nondecreasing (g ∘ f)) :
nonincreasing g :=
take a₁ a₂, suppose a₁ ≤ a₂,
have g (f (h a₁)) ≥ g (f (h a₂)), from H₃ (H₂ this),
show g a₁ ≥ g a₂, by rewrite *H₁ at this; apply this
theorem nondecreasing_of_nonincreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : nonincreasing h) (H₃ : nonincreasing (g ∘ f)) :
nondecreasing g :=
take a₁ a₂, suppose a₁ ≤ a₂,
have g (f (h a₁)) ≤ g (f (h a₂)), from H₃ (H₂ this),
show g a₁ ≤ g a₂, by rewrite *H₁ at this; apply this
theorem nonincreasing_of_nonincreasing_comp_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : nondecreasing h) (H₃ : nonincreasing (g ∘ f)) :
nonincreasing g :=
take a₁ a₂, suppose a₁ ≤ a₂,
have g (f (h a₁)) ≥ g (f (h a₂)), from H₃ (H₂ this),
show g a₁ ≥ g a₂, by rewrite *H₁ at this; apply this
end
section
variables [weak_order A] [linear_strong_order_pair B] [linear_strong_order_pair C]
theorem nondecreasing_comp_iff_nondecreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) :
nondecreasing (g ∘ f) ↔ nondecreasing f :=
have H₃ : nondecreasing g, from nondecreasing_of_left_inverse H₁ H₂,
iff.intro
(nondecreasing_of_nondecreasing_comp_right H₁ (nondecreasing_of_strictly_increasing H₂))
(nondecreasing_comp_nondec_nondec H₃)
theorem nondecreasing_comp_iff_nonincreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) :
nondecreasing (g ∘ f) ↔ nonincreasing f :=
have H₃ : nonincreasing g, from nonincreasing_of_left_inverse H₁ H₂,
iff.intro
(nonincreasing_of_nondecreasing_comp_right H₁ (nonincreasing_of_strictly_decreasing H₂))
(nondecreasing_comp_noninc_noninc H₃)
theorem nonincreasing_comp_iff_nonincreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_increasing h) :
nonincreasing (g ∘ f) ↔ nonincreasing f :=
have H₃ : nondecreasing g, from nondecreasing_of_left_inverse H₁ H₂,
iff.intro
(nonincreasing_of_nonincreasing_comp_right H₁ (nondecreasing_of_strictly_increasing H₂))
(nonincreasing_comp_nondec_noninc H₃)
theorem nonincreasing_comp_iff' {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) :
nonincreasing (g ∘ f) ↔ nondecreasing f :=
have H₃ : nonincreasing g, from nonincreasing_of_left_inverse H₁ H₂,
iff.intro
(nondecreasing_of_nonincreasing_comp_right H₁ (nonincreasing_of_strictly_decreasing H₂))
(nonincreasing_comp_noninc_nondec H₃)
end
section
variables [linear_strong_order_pair A] [linear_strong_order_pair B] [weak_order C]
theorem nondecreasing_comp_iff'' {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
nondecreasing (g ∘ f) ↔ nondecreasing g :=
have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂,
iff.intro
(nondecreasing_of_nondecreasing_comp_left H₁ H₃)
(λ H, nondecreasing_comp_nondec_nondec H (nondecreasing_of_strictly_increasing H₂))
theorem nondecreasing_comp_iff''' {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
nondecreasing (g ∘ f) ↔ nonincreasing g :=
have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂,
iff.intro
(nonincreasing_of_nondecreasing_comp_left H₁ H₃)
(λ H, nondecreasing_comp_noninc_noninc H (nonincreasing_of_strictly_decreasing H₂))
theorem nonincreasing_comp_iff'' {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
nonincreasing (g ∘ f) ↔ nondecreasing g :=
have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂,
iff.intro
(nondecreasing_of_nonincreasing_comp_left H₁ H₃)
(λ H, nonincreasing_comp_nondec_noninc H (nonincreasing_of_strictly_decreasing H₂))
theorem nonincreasing_comp_iff''' {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
nonincreasing (g ∘ f) ↔ nonincreasing g :=
have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂,
iff.intro
(nonincreasing_of_nonincreasing_comp_left H₁ H₃)
(λ H, nonincreasing_comp_noninc_nondec H (nondecreasing_of_strictly_increasing H₂))
end

107
library/algebra/order.lean
View file

@ -6,9 +6,9 @@ Author: Jeremy Avigad
Weak orders "≤", strict orders "<", and structures that include both.
-/
import logic.eq logic.connectives algebra.binary algebra.priority
open eq eq.ops
open eq eq.ops function
variable {A : Type}
variables {A : Type}
/- weak orders -/
@ -18,8 +18,7 @@ structure weak_order [class] (A : Type) extends has_le A :=
(le_antisymm : ∀a b, le a b → le b a → a = b)
section
variable [s : weak_order A]
include s
variables [weak_order A]
theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
@ -38,8 +37,13 @@ end
structure linear_weak_order [class] (A : Type) extends weak_order A :=
(le_total : ∀a b, le a b ∨ le b a)
theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ∨ b ≤ a :=
!linear_weak_order.le_total
section
variables [linear_weak_order A]
theorem le.total (a b : A) : a ≤ b ∨ b ≤ a := !linear_weak_order.le_total
theorem le_of_not_ge {a b : A} (H : ¬ a ≥ b) : a ≤ b := or.resolve_left !le.total H
end
/- strict orders -/
@ -48,8 +52,7 @@ structure strict_order [class] (A : Type) extends has_lt A :=
(lt_trans : ∀a b c, lt a b → lt b c → lt a c)
section
variable [s : strict_order A]
include s
variable [strict_order A]
theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl -- alternate syntax
@ -131,55 +134,59 @@ structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
(lt_irrefl : ∀ a, ¬ lt a a)
theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ∨ a = b :=
!strong_order_pair.le_iff_lt_or_eq
section strong_order_pair
variable [strong_order_pair A]
theorem lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
iff.mp le_iff_lt_or_eq le_ab
theorem le_iff_lt_or_eq {a b : A} : a ≤ b ↔ a < b ∨ a = b :=
!strong_order_pair.le_iff_lt_or_eq
theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b :=
iff.mpr le_iff_lt_or_eq lt_or_eq
theorem lt_or_eq_of_le {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
iff.mp le_iff_lt_or_eq le_ab
private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
!strong_order_pair.lt_irrefl
theorem le_of_lt_or_eq {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b :=
iff.mpr le_iff_lt_or_eq lt_or_eq
private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b :=
take Hlt, le_of_lt_or_eq (or.inl Hlt)
private theorem lt_irrefl' (a : A) : ¬ a < a :=
!strong_order_pair.lt_irrefl
private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
iff.intro
(take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl'))
(take Hand,
have Hor : a < b ∨ a = b, from lt_or_eq_of_le (and.left Hand),
or_resolve_left Hor (and.right Hand))
private theorem le_of_lt' (a b : A) : a < b → a ≤ b :=
take Hlt, le_of_lt_or_eq (or.inl Hlt)
theorem lt_of_le_of_ne [s : strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b :=
take H1 H2, iff.mpr lt_iff_le_and_ne (and.intro H1 H2)
private theorem lt_iff_le_and_ne {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
iff.intro
(take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl'))
(take Hand,
have Hor : a < b ∨ a = b, from lt_or_eq_of_le (and.left Hand),
or_resolve_left Hor (and.right Hand))
private theorem ne_of_lt' [s : strong_order_pair A] {a b : A} (H : a < b) : a ≠ b :=
and.right ((iff.mp lt_iff_le_and_ne) H)
theorem lt_of_le_of_ne {a b : A} : a ≤ b → a ≠ b → a < b :=
take H1 H2, iff.mpr lt_iff_le_and_ne (and.intro H1 H2)
private theorem lt_of_lt_of_le' [s : strong_order_pair A] (a b c : A) : a < b → b ≤ c → a < c :=
assume lt_ab : a < b,
assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba,
show false, from ne_of_lt' lt_ab eq_ab,
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
private theorem ne_of_lt' {a b : A} (H : a < b) : a ≠ b :=
and.right ((iff.mp lt_iff_le_and_ne) H)
theorem lt_of_le_of_lt' [s : strong_order_pair A] (a b c : A) : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b,
assume lt_bc : b < c,
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt' _ _ lt_bc),
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
have eq_bc : b = c, from le.antisymm (le_of_lt' _ _ lt_bc) le_cb,
show false, from ne_of_lt' lt_bc eq_bc,
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
private theorem lt_of_lt_of_le' (a b c : A) : a < b → b ≤ c → a < c :=
assume lt_ab : a < b,
assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba,
show false, from ne_of_lt' lt_ab eq_ab,
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
theorem lt_of_le_of_lt' (a b c : A) : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b,
assume lt_bc : b < c,
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt' _ _ lt_bc),
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
have eq_bc : b = c, from le.antisymm (le_of_lt' _ _ lt_bc) le_cb,
show false, from ne_of_lt' lt_bc eq_bc,
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
end strong_order_pair
definition strong_order_pair.to_order_pair [trans_instance]
[s : strong_order_pair A] : order_pair A :=
@ -201,9 +208,8 @@ definition linear_strong_order_pair.to_linear_order_pair [trans_instance]
⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄
section
variable [s : linear_strong_order_pair A]
variable [linear_strong_order_pair A]
variables (a b c : A)
include s
theorem lt.trichotomy : a < b ∨ a = b ∨ b < a :=
or.elim (le.total a b)
@ -287,7 +293,6 @@ section
exact or.inr a_1
end
-- testing equality first may result in more definitional equalities
definition lt.cases {B : Type} (a b : A) (t_lt t_eq t_gt : B) : B :=
if a = b then t_eq else (if a < b then t_lt else t_gt)

145
library/algebra/ordered_group.lean
View file

@ -7,10 +7,10 @@ Partially ordered additive groups, modeled on Isabelle's library. These classes
if necessary.
-/
import logic.eq data.unit data.sigma data.prod
import algebra.binary algebra.group algebra.order
import algebra.binary algebra.group algebra.order algebra.monotone
open eq eq.ops -- note: ⁻¹ will be overloaded
variable {A : Type}
variables {A B : Type}
/- partially ordered monoids, such as the natural numbers -/
@ -22,9 +22,8 @@ structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid
(lt_of_add_lt_add_left : ∀a b c, lt (add a b) (add a c) → lt b c)
section
variables [s : ordered_cancel_comm_monoid A]
variables [ordered_cancel_comm_monoid A]
variables {a b c d e : A}
include s
theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b :=
!ordered_cancel_comm_monoid.add_lt_add_left H c
@ -190,6 +189,18 @@ section
theorem add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c :=
!add_zero ▸ add_lt_add Hbc Ha
theorem strictly_increasing_add_left (c : A) : strictly_increasing (λ x, x + c) :=
take x₁ x₂, assume H, add_lt_add_right H c
theorem strictly_increasing_add_right (c : A) : strictly_increasing (λ x, c + x) :=
take x₁ x₂, assume H, add_lt_add_left H c
theorem nondecreasing_add_left (c : A) : nondecreasing (λ x, x + c) :=
take x₁ x₂, assume H, add_le_add_right H c
theorem nondecreasing_add_right (c : A) : nondecreasing (λ x, c + x) :=
take x₁ x₂, assume H, add_le_add_left H c
end
/- ordered cancelative commutative monoids with a decidable linear order -/
@ -198,9 +209,8 @@ structure decidable_linear_ordered_cancel_comm_monoid [class] (A : Type)
extends ordered_cancel_comm_monoid A, decidable_linear_order A
section
variables [s : decidable_linear_ordered_cancel_comm_monoid A]
variables [decidable_linear_ordered_cancel_comm_monoid A]
variables {a b c d e : A}
include s
theorem min_add_add_left : min (a + b) (a + c) = a + min b c :=
eq.symm (eq_min
@ -257,8 +267,7 @@ definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s
lt_of_add_lt_add_left := @ordered_comm_group.lt_of_add_lt_add_left A _⦄
section
variables [s : ordered_comm_group A] (a b c d e : A)
include s
variables [ordered_comm_group A] (a b c d e : A)
theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a :=
have H1 : 0 ≤ -a + b, from !add.left_inv ▸ !(add_le_add_left H),
@ -603,13 +612,127 @@ section
end
theorem sub_le_of_nonneg {b : A} (H : b ≥ 0) : a - b ≤ a :=
add_le_of_le_of_nonpos (le.refl a) (neg_nonpos_of_nonneg H)
add_le_of_le_of_nonpos (le.refl a) (neg_nonpos_of_nonneg H)
theorem sub_lt_of_pos {b : A} (H : b > 0) : a - b < a :=
add_lt_of_le_of_neg (le.refl a) (neg_neg_of_pos H)
add_lt_of_le_of_neg (le.refl a) (neg_neg_of_pos H)
theorem neg_add_neg_le_neg_of_pos {a : A} (H : a > 0) : -a + -a ≤ -a :=
!neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H))
!neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H))
variable (A)
theorem strictly_decreasing_neg : strictly_decreasing (λ x : A, -x) :=
@neg_lt_neg A _
variable {A}
section
variable [strict_order B]
theorem strictly_decreasing_neg_of_strictly_increasing {f : B → A}
(H : strictly_increasing f) : strictly_decreasing (λ x, - f x) :=
strictly_decreasing_comp_dec_inc (strictly_decreasing_neg A) H
theorem strictly_increasing_neg_of_strictly_decreasing {f : B → A}
(H : strictly_decreasing f) : strictly_increasing (λ x, - f x) :=
strictly_increasing_comp_dec_dec (strictly_decreasing_neg A) H
theorem strictly_decreasing_of_strictly_increasing_neg {f : B → A}
(H : strictly_increasing (λ x, - f x)) : strictly_decreasing f :=
strictly_decreasing_of_strictly_increasing_comp_right (left_inverse_neg A)
(strictly_decreasing_neg A) H
theorem strictly_increasing_of_strictly_decreasing_neg {f : B → A}
(H : strictly_decreasing (λ x, - f x)) : strictly_increasing f :=
strictly_increasing_of_strictly_decreasing_comp_right (left_inverse_neg A)
(strictly_decreasing_neg A) H
theorem strictly_decreasing_neg_iff {f : B → A} :
strictly_decreasing (λ x, - f x) ↔ strictly_increasing f :=
iff.intro strictly_increasing_of_strictly_decreasing_neg
strictly_decreasing_neg_of_strictly_increasing
theorem strictly_increasing_neg_iff {f : B → A} :
strictly_increasing (λ x, - f x) ↔ strictly_decreasing f :=
iff.intro strictly_decreasing_of_strictly_increasing_neg
strictly_increasing_neg_of_strictly_decreasing
theorem strictly_decreasing_neg_of_strictly_increasing' {f : A → B}
(H : strictly_increasing f) : strictly_decreasing (λ x, f (-x)) :=
strictly_decreasing_comp_inc_dec H (strictly_decreasing_neg A)
theorem strictly_increasing_neg_of_strictly_decreasing' {f : A → B}
(H : strictly_decreasing f) : strictly_increasing (λ x, f (-x)) :=
strictly_increasing_comp_dec_dec H (strictly_decreasing_neg A)
theorem strictly_decreasing_of_strictly_increasing_neg' {f : A → B}
(H : strictly_increasing (λ x, f (-x))) : strictly_decreasing f :=
strictly_decreasing_of_strictly_increasing_comp_left (left_inverse_neg A)
(strictly_decreasing_neg A) H
theorem strictly_increasing_of_strictly_decreasing_neg' {f : A → B}
(H : strictly_decreasing (λ x, f (-x))) : strictly_increasing f :=
strictly_increasing_of_strictly_decreasing_comp_left (left_inverse_neg A)
(strictly_decreasing_neg A) H
theorem strictly_decreasing_neg_iff' {f : A → B} :
strictly_decreasing (λ x, f (-x)) ↔ strictly_increasing f :=
iff.intro strictly_increasing_of_strictly_decreasing_neg'
strictly_decreasing_neg_of_strictly_increasing'
theorem strictly_increasing_neg_iff' {f : A → B} :
strictly_increasing (λ x, f (-x)) ↔ strictly_decreasing f :=
iff.intro strictly_decreasing_of_strictly_increasing_neg'
strictly_increasing_neg_of_strictly_decreasing'
end
section
variable [weak_order B]
theorem nondecreasing_of_neg_nonincreasing {f : B → A} (H : nonincreasing (λ x, -f x)) :
nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂, le_of_neg_le_neg (H this)
theorem nonincreasing_neg {f : B → A} (H : nondecreasing f) : nonincreasing (λ x, -f x) :=
take a₁ a₂, suppose a₁ ≤ a₂, neg_le_neg (H this)
theorem nonincreasing_neg_iff (f : B → A) : nonincreasing (λ x, - f x) ↔ nondecreasing f :=
iff.intro nondecreasing_of_neg_nonincreasing nonincreasing_neg
theorem nonincreasing_of_neg_nondecreasing {f : B → A} (H : nondecreasing (λ x, -f x)) :
nonincreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂, le_of_neg_le_neg (H this)
theorem nondecreasing_neg {f : B → A} (H : nonincreasing f) : nondecreasing (λ x, -f x) :=
take a₁ a₂, suppose a₁ ≤ a₂, neg_le_neg (H this)
theorem nondecreasing_neg_iff (f : B → A) : nondecreasing (λ x, - f x) ↔ nonincreasing f :=
iff.intro nonincreasing_of_neg_nondecreasing nondecreasing_neg
theorem nondecreasing_of_neg_nonincreasing' {f : A → B} (H : nonincreasing (λ x, f (-x))) :
nondecreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have f(-(-a₁)) ≤ f(-(-a₂)), from H (neg_le_neg this),
by rewrite *neg_neg at this; exact this
theorem nonincreasing_neg' {f : A → B} (H : nondecreasing f) : nonincreasing (λ x, f (-x)) :=
take a₁ a₂, suppose a₁ ≤ a₂, H (neg_le_neg this)
theorem nonincreasing_neg_iff' (f : A → B) : nonincreasing (λ x, f (- x)) ↔ nondecreasing f :=
iff.intro nondecreasing_of_neg_nonincreasing' nonincreasing_neg'
theorem nonincreasing_of_neg_nondecreasing' {f : A → B} (H : nondecreasing (λ x, f (-x))) :
nonincreasing f :=
take a₁ a₂, suppose a₁ ≤ a₂,
have f(-(-a₁)) ≥ f(-(-a₂)), from H (neg_le_neg this),
by rewrite *neg_neg at this; exact this
theorem nondecreasing_neg' {f : A → B} (H : nonincreasing f) : nondecreasing (λ x, f (-x)) :=
take a₁ a₂, suppose a₁ ≤ a₂, H (neg_le_neg this)
theorem nondecreasing_neg_iff' (f : A → B) : nondecreasing (λ x, f (- x)) ↔ nonincreasing f :=
iff.intro nonincreasing_of_neg_nondecreasing' nondecreasing_neg'
end
end
/- linear ordered group with decidable order -/

47
library/data/nat/order.lean
View file

@ -228,6 +228,52 @@ lt.base n
lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
assume Plt, lt.trans Plt (self_lt_succ j)
/- increasing and decreasing functions -/
section
variables {A : Type} [strict_order A] {f : ℕ → A}
theorem strictly_increasing_of_forall_lt_succ (H : ∀ i, f i < f (succ i)) : strictly_increasing f :=
take i j,
nat.induction_on j
(suppose i < 0, absurd this !not_lt_zero)
(take j', assume ih, suppose i < succ j',
or.elim (lt_or_eq_of_le (le_of_lt_succ this))
(suppose i < j', lt.trans (ih this) (H j'))
(suppose i = j', by rewrite this; apply H))
theorem strictly_decreasing_of_forall_gt_succ (H : ∀ i, f i > f (succ i)) : strictly_decreasing f :=
take i j,
nat.induction_on j
(suppose i < 0, absurd this !not_lt_zero)
(take j', assume ih, suppose i < succ j',
or.elim (lt_or_eq_of_le (le_of_lt_succ this))
(suppose i < j', lt.trans (H j') (ih this))
(suppose i = j', by rewrite this; apply H))
end
section
variables {A : Type} [weak_order A] {f : ℕ → A}
theorem nondecreasing_of_forall_le_succ (H : ∀ i, f i ≤ f (succ i)) : nondecreasing f :=
take i j,
nat.induction_on j
(suppose i ≤ 0, have i = 0, from eq_zero_of_le_zero this, by rewrite this; apply le.refl)
(take j', assume ih, suppose i ≤ succ j',
or.elim (le_or_eq_succ_of_le_succ this)
(suppose i ≤ j', le.trans (ih this) (H j'))
(suppose i = succ j', by rewrite this; apply le.refl))
theorem nonincreasing_of_forall_ge_succ (H : ∀ i, f i ≥ f (succ i)) : nonincreasing f :=
take i j,
nat.induction_on j
(suppose i ≤ 0, have i = 0, from eq_zero_of_le_zero this, by rewrite this; apply le.refl)
(take j', assume ih, suppose i ≤ succ j',
or.elim (le_or_eq_succ_of_le_succ this)
(suppose i ≤ j', le.trans (H j') (ih this))
(suppose i = succ j', by rewrite this; apply le.refl))
end
/- other forms of induction -/
protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
@ -458,7 +504,6 @@ section least_and_greatest
rewrite Heq at Hi,
apply absurd (least_of_bound P Hi) Pnsm
end
theorem least_lt {n i : ℕ} (ltin : i < n) (Hi : P i) : least P n < n :=
lt_of_le_of_lt (ge_least_of_lt P ltin Hi) ltin

48
library/theories/analysis/real_limit.lean
View file

@ -420,17 +420,6 @@ section monotone_sequences
open real set
variable {X : ℕ → ℝ}
definition nondecreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≤ X j
proposition nondecreasing_of_forall_le_succ (H : ∀ i, X i ≤ X (succ i)) : nondecreasing X :=
take i j, suppose i ≤ j,
have ∀ n, X i ≤ X (i + n), from
take n, nat.induction_on n
(by rewrite nat.add_zero; apply le.refl)
(take n, assume ih, le.trans ih (H (i + n))),
have X i ≤ X (i + (j - i)), from !this,
by rewrite [add_sub_of_le `i ≤ j` at this]; exact this
proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ}
(Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) in ℕ :=
let sX := sup (X ' univ) in
@ -459,41 +448,6 @@ exists.intro i
have sX - X j < ε, from sub_lt_left_of_lt_add this,
show (abs (X j - sX)) < ε, by rewrite eq₁; exact this)
definition nonincreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≥ X j
proposition nodecreasing_of_nonincreasing_neg (nonincX : nonincreasing (λ n, - X n)) :
nondecreasing (λ n, X n) :=
take i j, suppose i ≤ j,
show X i ≤ X j, from le_of_neg_le_neg (nonincX this)
proposition noincreasing_neg_of_nondecreasing (nondecX : nondecreasing X) :
nonincreasing (λ n, - X n) :=
take i j, suppose i ≤ j,
show - X i ≥ - X j, from neg_le_neg (nondecX this)
proposition nonincreasing_neg_iff (X : ℕ → ℝ) : nonincreasing (λ n, - X n) ↔ nondecreasing X :=
iff.intro nodecreasing_of_nonincreasing_neg noincreasing_neg_of_nondecreasing
proposition nonincreasing_of_nondecreasing_neg (nondecX : nondecreasing (λ n, - X n)) :
nonincreasing (λ n, X n) :=
take i j, suppose i ≤ j,
show X i ≥ X j, from le_of_neg_le_neg (nondecX this)
proposition nodecreasing_neg_of_nonincreasing (nonincX : nonincreasing X) :
nondecreasing (λ n, - X n) :=
take i j, suppose i ≤ j,
show - X i ≤ - X j, from neg_le_neg (nonincX this)
proposition nondecreasing_neg_iff (X : ℕ → ℝ) : nondecreasing (λ n, - X n) ↔ nonincreasing X :=
iff.intro nonincreasing_of_nondecreasing_neg nodecreasing_neg_of_nonincreasing
proposition nonincreasing_of_forall_succ_le (H : ∀ i, X (succ i) ≤ X i) : nonincreasing X :=
begin
rewrite -nondecreasing_neg_iff,
show nondecreasing (λ n : ℕ, - X n), from
nondecreasing_of_forall_le_succ (take i, neg_le_neg (H i))
end
proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ}
(Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) in ℕ :=
have H₁ : ∃ x, x ∈ X ' univ, from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
@ -527,7 +481,7 @@ let aX := (λ n, (abs x)^n),
iaX := real.inf (aX ' univ),
asX := (λ n, (abs x)^(succ n)) in
have noninc_aX : nonincreasing aX, from
nonincreasing_of_forall_succ_le
nonincreasing_of_forall_ge_succ
(take i,
have (abs x) * (abs x)^i ≤ 1 * (abs x)^i,
from mul_le_mul_of_nonneg_right (le_of_lt H) (!pow_nonneg_of_nonneg !abs_nonneg),