diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md index dd4e1816ae..3e18acd484 100644 --- a/library/algebra/algebra.md +++ b/library/algebra/algebra.md @@ -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) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index f7c217fda3..6664652c56 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -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 diff --git a/library/algebra/group.lean b/library/algebra/group.lean index a6b9e02db5..26ec5d090b 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -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 diff --git a/library/algebra/homomorphism.lean b/library/algebra/homomorphism.lean index 1e85a7f659..d26d9d6cd2 100644 --- a/library/algebra/homomorphism.lean +++ b/library/algebra/homomorphism.lean @@ -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 diff --git a/library/algebra/monotone.lean b/library/algebra/monotone.lean new file mode 100644 index 0000000000..36cb0a4dad --- /dev/null +++ b/library/algebra/monotone.lean @@ -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 diff --git a/library/algebra/order.lean b/library/algebra/order.lean index bfe0a67e8a..3d722f64ac 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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) diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 7ac936b124..f8ec18b516 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -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 -/ diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index d6129dfd8d..5b6842cbaa 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -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 diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index e0704e58b0..011518a088 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -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),