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

fix(library/algebra/monotone): fix theorem names

Browse source
This commit is contained in:
Jeremy Avigad 2016-03-02 22:54:51 -05:00
parent 4050892889
commit dc6cd71236
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/algebra/monotone.lean
View file

@ -372,7 +372,7 @@ section
(nonincreasing_of_nonincreasing_comp_right H₁ (nondecreasing_of_strictly_increasing H₂)) (nonincreasing_of_nonincreasing_comp_right H₁ (nondecreasing_of_strictly_increasing H₂))
(nonincreasing_comp_nondec_noninc H₃) (nonincreasing_comp_nondec_noninc H₃)
theorem nonincreasing_comp_iff' {g : B → C} {f : A → B} {h : C → B} theorem nonincreasing_comp_iff_nondecreasing_right {g : B → C} {f : A → B} {h : C → B}
(H₁ : left_inverse h g) (H₂ : strictly_decreasing h) : (H₁ : left_inverse h g) (H₂ : strictly_decreasing h) :
nonincreasing (g ∘ f) ↔ nondecreasing f := nonincreasing (g ∘ f) ↔ nondecreasing f :=
have H₃ : nonincreasing g, from nonincreasing_of_left_inverse H₁ H₂, have H₃ : nonincreasing g, from nonincreasing_of_left_inverse H₁ H₂,
@ -384,7 +384,7 @@ end
section section
variables [linear_strong_order_pair A] [linear_strong_order_pair B] [weak_order C] 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} theorem nondecreasing_comp_iff_nondecreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) : (H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
nondecreasing (g ∘ f) ↔ nondecreasing g := nondecreasing (g ∘ f) ↔ nondecreasing g :=
have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂, have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂,
@ -392,7 +392,7 @@ section
(nondecreasing_of_nondecreasing_comp_left H₁ H₃) (nondecreasing_of_nondecreasing_comp_left H₁ H₃)
(λ H, nondecreasing_comp_nondec_nondec H (nondecreasing_of_strictly_increasing 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} theorem nondecreasing_comp_iff_nonincreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) : (H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
nondecreasing (g ∘ f) ↔ nonincreasing g := nondecreasing (g ∘ f) ↔ nonincreasing g :=
have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂, have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂,
@ -400,7 +400,7 @@ section
(nonincreasing_of_nondecreasing_comp_left H₁ H₃) (nonincreasing_of_nondecreasing_comp_left H₁ H₃)
(λ H, nondecreasing_comp_noninc_noninc H (nonincreasing_of_strictly_decreasing 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} theorem nonincreasing_comp_iff_nondecreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_decreasing f) : (H₁ : left_inverse f h) (H₂ : strictly_decreasing f) :
nonincreasing (g ∘ f) ↔ nondecreasing g := nonincreasing (g ∘ f) ↔ nondecreasing g :=
have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂, have H₃ : nonincreasing h, from nonincreasing_of_left_inverse H₁ H₂,
@ -408,7 +408,7 @@ section
(nondecreasing_of_nonincreasing_comp_left H₁ H₃) (nondecreasing_of_nonincreasing_comp_left H₁ H₃)
(λ H, nonincreasing_comp_nondec_noninc H (nonincreasing_of_strictly_decreasing 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} theorem nonincreasing_comp_iff_nonincreasing_left {g : B → C} {f : A → B} {h : B → A}
(H₁ : left_inverse f h) (H₂ : strictly_increasing f) : (H₁ : left_inverse f h) (H₂ : strictly_increasing f) :
nonincreasing (g ∘ f) ↔ nonincreasing g := nonincreasing (g ∘ f) ↔ nonincreasing g :=
have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂, have H₃ : nondecreasing h, from nondecreasing_of_left_inverse H₁ H₂,