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

refactor(library/algebra/order.lean): rename a field in an order structure

Browse source
This commit is contained in:
Jeremy Avigad 2015-04-27 13:33:21 -04:00 committed by Leonardo de Moura
parent d8e40d90d6
commit 7a1064b7e8
4 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/algebra/order.lean
View file

@ -116,7 +116,7 @@ wf.rec_on x H
/- structures with a weak and a strict order -/ /- structures with a weak and a strict order -/
structure order_pair [class] (A : Type) extends weak_order A, has_lt A := structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(lt_iff_le_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b)) (lt_iff_le_and_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b))
section section
variable [s : order_pair A] variable [s : order_pair A]
@ -124,7 +124,7 @@ section
include s include s
theorem lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b) := theorem lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b) :=
!order_pair.lt_iff_le_ne !order_pair.lt_iff_le_and_ne
theorem le_of_lt (H : a < b) : a ≤ b := theorem le_of_lt (H : a < b) : a ≤ b :=
and.elim_left (iff.mp lt_iff_le_and_ne H) and.elim_left (iff.mp lt_iff_le_and_ne H)
@ -243,10 +243,10 @@ iff.intro
definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] : definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] :
strong_order_pair A := strong_order_pair A :=
⦃ strong_order_pair, s, ⦃ strong_order_pair, s,
le_refl := le_refl s, le_refl := le_refl s,
le_trans := le_trans s, le_trans := le_trans s,
le_antisymm := le_antisymm s, le_antisymm := le_antisymm s,
lt_iff_le_ne := lt_iff_le_ne s ⦄ lt_iff_le_and_ne := lt_iff_le_ne s ⦄
/- linear orders -/ /- linear orders -/

2
library/data/int/order.lean
View file

@ -229,7 +229,7 @@ section
le_trans := @le.trans, le_trans := @le.trans,
le_antisymm := @le.antisymm, le_antisymm := @le.antisymm,
lt := lt, lt := lt,
lt_iff_le_ne := lt_iff_le_and_ne, lt_iff_le_and_ne := lt_iff_le_and_ne,
add_le_add_left := @add_le_add_left, add_le_add_left := @add_le_add_left,
mul_nonneg := @mul_nonneg, mul_nonneg := @mul_nonneg,
mul_pos := @mul_pos, mul_pos := @mul_pos,

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

@ -158,7 +158,7 @@ section
le_antisymm := @le.antisymm, le_antisymm := @le.antisymm,
le_total := @le.total, le_total := @le.total,
le_iff_lt_or_eq := @le_iff_lt_or_eq, le_iff_lt_or_eq := @le_iff_lt_or_eq,
lt_iff_le_ne := lt_iff_le_and_ne, lt_iff_le_and_ne := lt_iff_le_and_ne,
add_le_add_left := @add_le_add_left, add_le_add_left := @add_le_add_left,
le_of_add_le_add_left := @le_of_add_le_add_left, le_of_add_le_add_left := @le_of_add_le_add_left,
zero_ne_one := ne.symm (succ_ne_zero zero), zero_ne_one := ne.symm (succ_ne_zero zero),

22
library/data/rat/order.lean
View file

@ -198,7 +198,7 @@ theorem mul_pos (H1 : a > 0) (H2 : b > 0) : a * b > 0 :=
have H : pos (a * b), from pos_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2), have H : pos (a * b), from pos_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2),
!sub_zero⁻¹ ▸ H !sub_zero⁻¹ ▸ H
definition has_decidable_lt [instance] : decidable_rel rat.lt := definition decidable_lt [instance] : decidable_rel rat.lt :=
take a b, decidable_pos (b - a) take a b, decidable_pos (b - a)
section section
@ -208,16 +208,16 @@ section
algebra.discrete_linear_ordered_field rat := algebra.discrete_linear_ordered_field rat :=
⦃algebra.discrete_linear_ordered_field, ⦃algebra.discrete_linear_ordered_field,
rat.discrete_field, rat.discrete_field,
le_refl := le.refl, le_refl := le.refl,
le_trans := @le.trans, le_trans := @le.trans,
le_antisymm := @le.antisymm, le_antisymm := @le.antisymm,
le_total := @le.total, le_total := @le.total,
lt_iff_le_ne := @lt_iff_le_and_ne, lt_iff_le_and_ne := @lt_iff_le_and_ne,
le_iff_lt_or_eq := @le_iff_lt_or_eq, le_iff_lt_or_eq := @le_iff_lt_or_eq,
add_le_add_left := @add_le_add_left, add_le_add_left := @add_le_add_left,
mul_nonneg := @mul_nonneg, mul_nonneg := @mul_nonneg,
mul_pos := @mul_pos, mul_pos := @mul_pos,
decidable_lt := @has_decidable_lt⦄ decidable_lt := @decidable_lt⦄
-- migrate from algebra with rat -- migrate from algebra with rat
end end