refactor(library,hott): remove unnecessary annotations
This commit is contained in:
parent
146edde5b3
commit
510168a387
47 changed files with 141 additions and 141 deletions
|
@ -12,7 +12,7 @@ open eq category is_trunc nat_trans iso is_equiv category.hom
|
|||
|
||||
namespace functor
|
||||
|
||||
definition precategory_functor [instance] [reducible] [constructor] (D C : Precategory)
|
||||
definition precategory_functor [instance] [constructor] (D C : Precategory)
|
||||
: precategory (functor C D) :=
|
||||
precategory.mk (λa b, nat_trans a b)
|
||||
(λ a b c g f, nat_trans.compose g f)
|
||||
|
|
|
@ -11,7 +11,7 @@ import ..category ..nat_trans hit.trunc
|
|||
open eq prod is_trunc functor sigma trunc iso prod.ops nat_trans
|
||||
|
||||
namespace category
|
||||
definition precategory_prod [constructor] [reducible] [instance] (obC obD : Type)
|
||||
definition precategory_prod [constructor] [instance] (obC obD : Type)
|
||||
[C : precategory obC] [D : precategory obD] : precategory (obC × obD) :=
|
||||
precategory.mk' (λ a b, hom a.1 b.1 × hom a.2 b.2)
|
||||
(λ a b c g f, (g.1 ∘ f.1, g.2 ∘ f.2))
|
||||
|
|
|
@ -82,7 +82,7 @@ namespace category
|
|||
end
|
||||
end set
|
||||
|
||||
definition category_Set [instance] [constructor] [reducible] : category Set :=
|
||||
definition category_Set [instance] [constructor] : category Set :=
|
||||
category.mk precategory_Set set.is_univalent_Set
|
||||
|
||||
definition Category_Set [reducible] [constructor] : Category :=
|
||||
|
|
|
@ -23,7 +23,7 @@ namespace category
|
|||
definition is_weak_equivalence [class] (F : C ⇒ D) :=
|
||||
fully_faithful F × essentially_surjective F
|
||||
|
||||
definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D)
|
||||
definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D)
|
||||
[H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
|
||||
!H
|
||||
|
||||
|
|
|
@ -39,11 +39,11 @@ namespace iso
|
|||
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
|
||||
include C
|
||||
|
||||
definition split_mono_of_is_iso [constructor] [instance] [priority 300] [reducible]
|
||||
definition split_mono_of_is_iso [constructor] [instance] [priority 300]
|
||||
(f : a ⟶ b) [H : is_iso f] : split_mono f :=
|
||||
split_mono.mk !left_inverse
|
||||
|
||||
definition split_epi_of_is_iso [constructor] [instance] [priority 300] [reducible]
|
||||
definition split_epi_of_is_iso [constructor] [instance] [priority 300]
|
||||
(f : a ⟶ b) [H : is_iso f] : split_epi f :=
|
||||
split_epi.mk !right_inverse
|
||||
|
||||
|
|
|
@ -152,7 +152,7 @@ namespace category
|
|||
attribute Precategory.carrier [coercion]
|
||||
attribute Precategory.struct [instance] [priority 10000] [coercion]
|
||||
-- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
|
||||
-- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
|
||||
-- definition precategory.struct [instance] [coercion] := Precategory.struct
|
||||
notation g ` ∘[`:60 C:0 `] `:0 f:60 :=
|
||||
@comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
|
||||
-- TODO: make this left associative
|
||||
|
|
|
@ -23,7 +23,7 @@ section division_ring
|
|||
|
||||
protected definition algebra.div (a b : A) : A := a * b⁻¹
|
||||
|
||||
definition division_ring_has_div [reducible] [instance] : has_div A :=
|
||||
definition division_ring_has_div [instance] : has_div A :=
|
||||
has_div.mk algebra.div
|
||||
|
||||
lemma division.def (a b : A) : a / b = a * b⁻¹ :=
|
||||
|
|
|
@ -462,7 +462,7 @@ section add_group
|
|||
-- TODO: derive corresponding facts for div in a field
|
||||
protected definition algebra.sub [reducible] (a b : A) : A := a + -b
|
||||
|
||||
definition add_group_has_sub [reducible] [instance] : has_sub A :=
|
||||
definition add_group_has_sub [instance] : has_sub A :=
|
||||
has_sub.mk algebra.sub
|
||||
|
||||
theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
|
||||
|
|
|
@ -75,7 +75,7 @@ section comm_semiring
|
|||
|
||||
protected definition algebra.dvd (a b : A) : Type := Σc, b = a * c
|
||||
|
||||
definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
|
||||
definition comm_semiring_has_dvd [instance] [priority algebra.prio] : has_dvd A :=
|
||||
has_dvd.mk algebra.dvd
|
||||
|
||||
theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
|
||||
|
|
|
@ -37,10 +37,10 @@ namespace sphere_index
|
|||
from 0 and up this comes from a coercion from num to sphere_index (via nat)
|
||||
-/
|
||||
|
||||
definition has_zero_sphere_index [instance] [reducible] : has_zero sphere_index :=
|
||||
definition has_zero_sphere_index [instance] : has_zero sphere_index :=
|
||||
has_zero.mk (succ minus_one)
|
||||
|
||||
definition has_one_sphere_index [instance] [reducible] : has_one sphere_index :=
|
||||
definition has_one_sphere_index [instance] : has_one sphere_index :=
|
||||
has_one.mk (succ (succ minus_one))
|
||||
|
||||
postfix `.+1`:(max+1) := sphere_index.succ
|
||||
|
@ -56,7 +56,7 @@ namespace sphere_index
|
|||
|
||||
infix `+1+`:65 := sphere_index.add
|
||||
|
||||
definition has_le_sphere_index [instance] [reducible] : has_le sphere_index :=
|
||||
definition has_le_sphere_index [instance] : has_le sphere_index :=
|
||||
has_le.mk leq
|
||||
|
||||
definition succ_le_succ {n m : sphere_index} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed
|
||||
|
|
|
@ -41,13 +41,13 @@ namespace nat
|
|||
| nat_refl : le a a -- use nat_refl to avoid overloading le.refl
|
||||
| step : Π {b}, le a b → le a (succ b)
|
||||
|
||||
definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
definition nat_has_le [instance] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
|
||||
protected definition le_refl [refl] : Π a : nat, a ≤ a :=
|
||||
le.nat_refl
|
||||
|
||||
protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
definition nat_has_lt [instance] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
|
||||
definition pred [unfold 1] (a : nat) : nat :=
|
||||
nat.cases_on a zero (λ a₁, a₁)
|
||||
|
@ -60,10 +60,10 @@ namespace nat
|
|||
protected definition mul (a b : nat) : nat :=
|
||||
nat.rec_on b zero (λ b₁ r, r + a)
|
||||
|
||||
definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat :=
|
||||
definition nat_has_sub [instance] [priority nat.prio] : has_sub nat :=
|
||||
has_sub.mk nat.sub
|
||||
|
||||
definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat :=
|
||||
definition nat_has_mul [instance] [priority nat.prio] : has_mul nat :=
|
||||
has_mul.mk nat.mul
|
||||
|
||||
/- properties of ℕ -/
|
||||
|
|
|
@ -34,7 +34,7 @@ namespace pos_num
|
|||
pos_num.lt a (succ b)
|
||||
end pos_num
|
||||
|
||||
definition pos_num_has_mul [instance] [reducible] : has_mul pos_num :=
|
||||
definition pos_num_has_mul [instance] : has_mul pos_num :=
|
||||
has_mul.mk pos_num.mul
|
||||
|
||||
namespace num
|
||||
|
@ -50,7 +50,7 @@ namespace num
|
|||
num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
|
||||
end num
|
||||
|
||||
definition num_has_mul [instance] [reducible] : has_mul num :=
|
||||
definition num_has_mul [instance] : has_mul num :=
|
||||
has_mul.mk num.mul
|
||||
|
||||
namespace num
|
||||
|
@ -80,5 +80,5 @@ namespace num
|
|||
num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
|
||||
end num
|
||||
|
||||
definition num_has_sub [instance] [reducible] : has_sub num :=
|
||||
definition num_has_sub [instance] : has_sub num :=
|
||||
has_sub.mk num.sub
|
||||
|
|
|
@ -41,13 +41,13 @@ definition bit0 [reducible] {A : Type} [s : has_add A] (a : A)
|
|||
definition bit1 [reducible] {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A :=
|
||||
add (bit0 a) one
|
||||
|
||||
definition num_has_zero [reducible] [instance] : has_zero num :=
|
||||
definition num_has_zero [instance] : has_zero num :=
|
||||
has_zero.mk num.zero
|
||||
|
||||
definition num_has_one [reducible] [instance] : has_one num :=
|
||||
definition num_has_one [instance] : has_one num :=
|
||||
has_one.mk (num.pos pos_num.one)
|
||||
|
||||
definition pos_num_has_one [reducible] [instance] : has_one pos_num :=
|
||||
definition pos_num_has_one [instance] : has_one pos_num :=
|
||||
has_one.mk (pos_num.one)
|
||||
|
||||
namespace pos_num
|
||||
|
@ -75,7 +75,7 @@ namespace pos_num
|
|||
b
|
||||
end pos_num
|
||||
|
||||
definition pos_num_has_add [reducible] [instance] : has_add pos_num :=
|
||||
definition pos_num_has_add [instance] : has_add pos_num :=
|
||||
has_add.mk pos_num.add
|
||||
|
||||
namespace num
|
||||
|
@ -85,7 +85,7 @@ namespace num
|
|||
num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
|
||||
end num
|
||||
|
||||
definition num_has_add [reducible] [instance] : has_add num :=
|
||||
definition num_has_add [instance] : has_add num :=
|
||||
has_add.mk num.add
|
||||
|
||||
definition std.priority.default : num := 1000
|
||||
|
@ -105,13 +105,13 @@ end nat
|
|||
attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
|
||||
[instance] [priority nat.prio]
|
||||
|
||||
definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
|
||||
definition nat_has_zero [instance] [priority nat.prio] : has_zero nat :=
|
||||
has_zero.mk nat.zero
|
||||
|
||||
definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
|
||||
definition nat_has_one [instance] [priority nat.prio] : has_one nat :=
|
||||
has_one.mk (nat.succ (nat.zero))
|
||||
|
||||
definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
|
||||
definition nat_has_add [instance] [priority nat.prio] : has_add nat :=
|
||||
has_add.mk nat.add
|
||||
|
||||
/-
|
||||
|
|
|
@ -23,10 +23,10 @@ namespace is_trunc
|
|||
|
||||
open trunc_index
|
||||
|
||||
definition has_zero_trunc_index [instance] [priority 2000] [reducible] : has_zero trunc_index :=
|
||||
definition has_zero_trunc_index [instance] [priority 2000] : has_zero trunc_index :=
|
||||
has_zero.mk (succ (succ minus_two))
|
||||
|
||||
definition has_one_trunc_index [instance] [priority 2000] [reducible] : has_one trunc_index :=
|
||||
definition has_one_trunc_index [instance] [priority 2000] : has_one trunc_index :=
|
||||
has_one.mk (succ (succ (succ minus_two)))
|
||||
|
||||
/-
|
||||
|
@ -55,14 +55,14 @@ namespace is_trunc
|
|||
definition leq [reducible] (n m : trunc_index) : Type₀ :=
|
||||
trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
|
||||
|
||||
definition has_le_trunc_index [instance] [priority 2000] [reducible] : has_le trunc_index :=
|
||||
definition has_le_trunc_index [instance] [priority 2000] : has_le trunc_index :=
|
||||
has_le.mk leq
|
||||
|
||||
end trunc_index
|
||||
|
||||
attribute trunc_index.tr_add [reducible]
|
||||
infix `+2+`:65 := trunc_index.add_plus_two
|
||||
definition has_add_trunc_index [instance] [priority 2000] [reducible] : has_add ℕ₋₂ :=
|
||||
definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ :=
|
||||
has_add.mk trunc_index.tr_add
|
||||
|
||||
namespace trunc_index
|
||||
|
|
|
@ -113,7 +113,7 @@ end pigeonhole-/
|
|||
protected definition zero [constructor] (n : nat) : fin (succ n) :=
|
||||
mk 0 !zero_lt_succ
|
||||
|
||||
definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) :=
|
||||
definition fin_has_zero [instance] (n : nat) : has_zero (fin (succ n)) :=
|
||||
has_zero.mk (fin.zero n)
|
||||
|
||||
definition val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl
|
||||
|
|
|
@ -48,10 +48,10 @@ notation `-[1+ ` n `]` := int.neg_succ_of_nat n -- for pretty-printing output
|
|||
|
||||
protected definition prio : num := num.pred nat.prio
|
||||
|
||||
definition int_has_zero [reducible] [instance] [priority int.prio] : has_zero int :=
|
||||
definition int_has_zero [instance] [priority int.prio] : has_zero int :=
|
||||
has_zero.mk (of_nat 0)
|
||||
|
||||
definition int_has_one [reducible] [instance] [priority int.prio] : has_one int :=
|
||||
definition int_has_one [instance] [priority int.prio] : has_one int :=
|
||||
has_one.mk (of_nat 1)
|
||||
|
||||
theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
|
||||
|
@ -89,9 +89,9 @@ protected definition mul : ℤ → ℤ → ℤ
|
|||
|
||||
/- notation -/
|
||||
|
||||
definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
|
||||
definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
|
||||
definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
|
||||
definition int_has_add [instance] [priority int.prio] : has_add int := has_add.mk int.add
|
||||
definition int_has_neg [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
|
||||
definition int_has_mul [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
|
||||
|
||||
lemma mul_of_nat_of_nat (m n : nat) : of_nat m * of_nat n = of_nat (m * n) :=
|
||||
rfl
|
||||
|
@ -575,10 +575,10 @@ protected definition integral_domain [reducible] [trans_instance] : integral_dom
|
|||
eq_zero_sum_eq_zero_of_mul_eq_zero := @int.eq_zero_sum_eq_zero_of_mul_eq_zero,
|
||||
is_set_carrier := is_set_of_decidable_eq⦄
|
||||
|
||||
definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int :=
|
||||
definition int_has_sub [instance] [priority int.prio] : has_sub int :=
|
||||
has_sub.mk has_sub.sub
|
||||
|
||||
definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
|
||||
definition int_has_dvd [instance] [priority int.prio] : has_dvd int :=
|
||||
has_dvd.mk has_dvd.dvd
|
||||
|
||||
/- additional properties -/
|
||||
|
|
|
@ -117,7 +117,7 @@ decidable_linear_ordered_semiring nat :=
|
|||
mul_lt_mul_of_pos_right := @nat.mul_lt_mul_of_pos_right,
|
||||
decidable_lt := nat.decidable_lt ⦄
|
||||
|
||||
definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat :=
|
||||
definition nat_has_dvd [instance] [priority nat.prio] : has_dvd nat :=
|
||||
has_dvd.mk has_dvd.dvd
|
||||
|
||||
theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
|
||||
|
|
|
@ -51,7 +51,7 @@ namespace category
|
|||
definition objects [coercion] [reducible] (C : Category) : Type
|
||||
:= Category.rec (fun c s, c) C
|
||||
|
||||
definition category_instance [instance] [coercion] [reducible] (C : Category) : category (objects C)
|
||||
definition category_instance [instance] [coercion] (C : Category) : category (objects C)
|
||||
:= Category.rec (fun c s, s) C
|
||||
|
||||
end category
|
||||
|
|
|
@ -22,7 +22,7 @@ section division_ring
|
|||
|
||||
protected definition algebra.div (a b : A) : A := a * b⁻¹
|
||||
|
||||
definition division_ring_has_div [reducible] [instance] : has_div A :=
|
||||
definition division_ring_has_div [instance] : has_div A :=
|
||||
has_div.mk algebra.div
|
||||
|
||||
lemma division.def [simp] (a b : A) : a / b = a * b⁻¹ :=
|
||||
|
|
|
@ -446,7 +446,7 @@ section add_group
|
|||
-- TODO: derive corresponding facts for div in a field
|
||||
protected definition algebra.sub [reducible] (a b : A) : A := a + -b
|
||||
|
||||
definition add_group_has_sub [reducible] [instance] : has_sub A :=
|
||||
definition add_group_has_sub [instance] : has_sub A :=
|
||||
has_sub.mk algebra.sub
|
||||
|
||||
theorem sub_eq_add_neg [simp] (a b : A) : a - b = a + -b := rfl
|
||||
|
|
|
@ -40,7 +40,7 @@ definition monoid.pow (a : A) : ℕ → A
|
|||
| 0 := 1
|
||||
| (n+1) := a * monoid.pow n
|
||||
|
||||
definition monoid_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
definition monoid_has_pow_nat [instance] : has_pow_nat A :=
|
||||
has_pow_nat.mk monoid.pow
|
||||
|
||||
theorem pow_zero (a : A) : a^0 = 1 := rfl
|
||||
|
|
|
@ -77,7 +77,7 @@ section comm_semiring
|
|||
|
||||
protected definition algebra.dvd (a b : A) : Prop := ∃c, b = a * c
|
||||
|
||||
definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
|
||||
definition comm_semiring_has_dvd [instance] [priority algebra.prio] : has_dvd A :=
|
||||
has_dvd.mk algebra.dvd
|
||||
|
||||
theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
|
||||
|
|
|
@ -14,7 +14,7 @@ section semiring
|
|||
variable [s : semiring A]
|
||||
include s
|
||||
|
||||
definition semiring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
definition semiring_has_pow_nat [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) :=
|
||||
|
@ -33,7 +33,7 @@ section integral_domain
|
|||
variable [s : integral_domain A]
|
||||
include s
|
||||
|
||||
definition integral_domain_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
definition integral_domain_has_pow_nat [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem eq_zero_of_pow_eq_zero {a : A} {m : ℕ} (H : a^m = 0) : a = 0 :=
|
||||
|
@ -151,7 +151,7 @@ section decidable_linear_ordered_comm_ring
|
|||
variable [s : decidable_linear_ordered_comm_ring A]
|
||||
include s
|
||||
|
||||
definition decidable_linear_ordered_comm_ring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
definition decidable_linear_ordered_comm_ring_has_pow_nat [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n :=
|
||||
|
|
|
@ -37,10 +37,10 @@ definition of_num [coercion] [reducible] (n : num) : ℂ := n
|
|||
|
||||
protected definition prio : num := num.pred real.prio
|
||||
|
||||
definition complex_has_zero [reducible] [instance] [priority complex.prio] : has_zero ℂ :=
|
||||
definition complex_has_zero [instance] [priority complex.prio] : has_zero ℂ :=
|
||||
has_zero.mk (of_nat 0)
|
||||
|
||||
definition complex_has_one [reducible] [instance] [priority complex.prio] : has_one ℂ :=
|
||||
definition complex_has_one [instance] [priority complex.prio] : has_one ℂ :=
|
||||
has_one.mk (of_nat 1)
|
||||
|
||||
theorem re_of_real (x : ℝ) : re (of_real x) = x := rfl
|
||||
|
@ -60,13 +60,13 @@ complex.mk
|
|||
|
||||
/- notation -/
|
||||
|
||||
definition complex_has_add [reducible] [instance] [priority complex.prio] : has_add complex :=
|
||||
definition complex_has_add [instance] [priority complex.prio] : has_add complex :=
|
||||
has_add.mk complex.add
|
||||
|
||||
definition complex_has_neg [reducible] [instance] [priority complex.prio] : has_neg complex :=
|
||||
definition complex_has_neg [instance] [priority complex.prio] : has_neg complex :=
|
||||
has_neg.mk complex.neg
|
||||
|
||||
definition complex_has_mul [reducible] [instance] [priority complex.prio] : has_mul complex :=
|
||||
definition complex_has_mul [instance] [priority complex.prio] : has_mul complex :=
|
||||
has_mul.mk complex.mul
|
||||
|
||||
protected theorem add_def (z w : ℂ) :
|
||||
|
@ -179,7 +179,7 @@ protected definition comm_ring [reducible] : comm_ring complex :=
|
|||
|
||||
local attribute complex.comm_ring [instance]
|
||||
|
||||
definition complex_has_sub [reducible] [instance] [priority complex.prio] : has_sub complex :=
|
||||
definition complex_has_sub [instance] [priority complex.prio] : has_sub complex :=
|
||||
has_sub.mk has_sub.sub
|
||||
|
||||
theorem of_real_sub (x y : ℝ) : of_real (x - y) = of_real x - of_real y :=
|
||||
|
@ -234,7 +234,7 @@ end
|
|||
|
||||
protected noncomputable definition inv (z : ℂ) : complex := conj z * of_real (cmod z)⁻¹
|
||||
|
||||
protected noncomputable definition complex_has_inv [reducible] [instance] [priority complex.prio] :
|
||||
protected noncomputable definition complex_has_inv [instance] [priority complex.prio] :
|
||||
has_inv complex := has_inv.mk complex.inv
|
||||
|
||||
protected theorem inv_def (z : ℂ) : z⁻¹ = conj z * of_real (cmod z)⁻¹ := rfl
|
||||
|
@ -252,7 +252,7 @@ classical.by_cases
|
|||
|
||||
noncomputable protected definition div (z w : ℂ) : ℂ := z * w⁻¹
|
||||
|
||||
noncomputable definition complex_has_div [instance] [reducible] [priority complex.prio] :
|
||||
noncomputable definition complex_has_div [instance] [priority complex.prio] :
|
||||
has_div complex :=
|
||||
has_div.mk complex.div
|
||||
|
||||
|
|
|
@ -88,7 +88,7 @@ end pigeonhole
|
|||
protected definition zero (n : nat) : fin (succ n) :=
|
||||
mk 0 !zero_lt_succ
|
||||
|
||||
definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) :=
|
||||
definition fin_has_zero [instance] (n : nat) : has_zero (fin (succ n)) :=
|
||||
has_zero.mk (fin.zero n)
|
||||
|
||||
theorem val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl
|
||||
|
|
|
@ -23,7 +23,7 @@ protected definition prio : num := num.succ std.priority.default
|
|||
protected definition is_inhabited [instance] : inhabited hf :=
|
||||
nat.is_inhabited
|
||||
|
||||
protected definition has_decidable_eq [reducible] [instance] : decidable_eq hf :=
|
||||
protected definition has_decidable_eq [instance] : decidable_eq hf :=
|
||||
nat.has_decidable_eq
|
||||
|
||||
definition of_finset (s : finset hf) : hf :=
|
||||
|
|
|
@ -48,10 +48,10 @@ notation `-[1+ ` n `]` := int.neg_succ_of_nat n -- for pretty-printing output
|
|||
|
||||
protected definition prio : num := num.pred nat.prio
|
||||
|
||||
definition int_has_zero [reducible] [instance] [priority int.prio] : has_zero int :=
|
||||
definition int_has_zero [instance] [priority int.prio] : has_zero int :=
|
||||
has_zero.mk (of_nat 0)
|
||||
|
||||
definition int_has_one [reducible] [instance] [priority int.prio] : has_one int :=
|
||||
definition int_has_one [instance] [priority int.prio] : has_one int :=
|
||||
has_one.mk (of_nat 1)
|
||||
|
||||
theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
|
||||
|
@ -89,9 +89,9 @@ protected definition mul : ℤ → ℤ → ℤ
|
|||
|
||||
/- notation -/
|
||||
|
||||
definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
|
||||
definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
|
||||
definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
|
||||
definition int_has_add [instance] [priority int.prio] : has_add int := has_add.mk int.add
|
||||
definition int_has_neg [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
|
||||
definition int_has_mul [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
|
||||
|
||||
lemma mul_of_nat_of_nat (m n : nat) : of_nat m * of_nat n = of_nat (m * n) :=
|
||||
rfl
|
||||
|
@ -536,10 +536,10 @@ protected definition integral_domain [reducible] [trans_instance] : integral_dom
|
|||
zero_ne_one := int.zero_ne_one,
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := @int.eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||||
|
||||
definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int :=
|
||||
definition int_has_sub [instance] [priority int.prio] : has_sub int :=
|
||||
has_sub.mk has_sub.sub
|
||||
|
||||
definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
|
||||
definition int_has_dvd [instance] [priority int.prio] : has_dvd int :=
|
||||
has_dvd.mk has_dvd.dvd
|
||||
|
||||
/- additional properties -/
|
||||
|
|
|
@ -23,7 +23,7 @@ sign b *
|
|||
| -[1+m] := -[1+ ((m:nat) / (nat_abs b))]
|
||||
end)
|
||||
|
||||
definition int_has_div [reducible] [instance] [priority int.prio] : has_div int :=
|
||||
definition int_has_div [instance] [priority int.prio] : has_div int :=
|
||||
has_div.mk int.div
|
||||
|
||||
lemma of_nat_div_eq (m : nat) (b : ℤ) : (of_nat m) / b = sign b * of_nat (m / (nat_abs b)) :=
|
||||
|
@ -42,7 +42,7 @@ rfl
|
|||
|
||||
protected definition mod (a b : ℤ) : ℤ := a - a / b * b
|
||||
|
||||
definition int_has_mod [reducible] [instance] [priority int.prio] : has_mod int :=
|
||||
definition int_has_mod [instance] [priority int.prio] : has_mod int :=
|
||||
has_mod.mk int.mod
|
||||
|
||||
|
||||
|
|
|
@ -16,12 +16,12 @@ namespace int
|
|||
private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false)
|
||||
protected definition le (a b : ℤ) : Prop := nonneg (b - a)
|
||||
|
||||
definition int_has_le [instance] [reducible] [priority int.prio]: has_le int :=
|
||||
definition int_has_le [instance] [priority int.prio]: has_le int :=
|
||||
has_le.mk int.le
|
||||
|
||||
protected definition lt (a b : ℤ) : Prop := (a + 1) ≤ b
|
||||
|
||||
definition int_has_lt [instance] [reducible] [priority int.prio]: has_lt int :=
|
||||
definition int_has_lt [instance] [priority int.prio]: has_lt int :=
|
||||
has_lt.mk int.lt
|
||||
|
||||
local attribute nonneg [reducible]
|
||||
|
@ -253,7 +253,7 @@ protected definition linear_ordered_comm_ring [reducible] [trans_instance] :
|
|||
zero_lt_one := int.zero_lt_one,
|
||||
add_lt_add_left := @int.add_lt_add_left⦄
|
||||
|
||||
protected definition decidable_linear_ordered_comm_ring [reducible] [instance] :
|
||||
protected definition decidable_linear_ordered_comm_ring [instance] :
|
||||
decidable_linear_ordered_comm_ring int :=
|
||||
⦃decidable_linear_ordered_comm_ring,
|
||||
int.linear_ordered_comm_ring,
|
||||
|
|
|
@ -9,7 +9,7 @@ import data.int.basic data.int.order data.int.div algebra.group_power data.nat.p
|
|||
|
||||
namespace int
|
||||
|
||||
definition int_has_pow_nat [reducible] [instance] [priority int.prio] : has_pow_nat int :=
|
||||
definition int_has_pow_nat [instance] [priority int.prio] : has_pow_nat int :=
|
||||
has_pow_nat.mk has_pow_nat.pow_nat
|
||||
|
||||
/-
|
||||
|
|
|
@ -68,16 +68,16 @@ protected definition mul (M : matrix A m n) (N : matrix A n p) : matrix A m p :=
|
|||
definition smul (a : A) (M : matrix A m n) : matrix A m n :=
|
||||
λ i j, a * M[i, j]
|
||||
|
||||
definition matrix_has_zero [reducible] [instance] (m n : nat) : has_zero (matrix A m n) :=
|
||||
definition matrix_has_zero [instance] (m n : nat) : has_zero (matrix A m n) :=
|
||||
has_zero.mk (matrix.zero m n)
|
||||
|
||||
definition matrix_has_one [reducible] [instance] (n : nat) : has_one (matrix A n n) :=
|
||||
definition matrix_has_one [instance] (n : nat) : has_one (matrix A n n) :=
|
||||
has_one.mk (identity n)
|
||||
|
||||
definition matrix_has_add [reducible] [instance] (m n : nat) : has_add (matrix A m n) :=
|
||||
definition matrix_has_add [instance] (m n : nat) : has_add (matrix A m n) :=
|
||||
has_add.mk matrix.add
|
||||
|
||||
definition matrix_has_mul [reducible] [instance] (n : nat) : has_mul (matrix A n n) :=
|
||||
definition matrix_has_mul [instance] (n : nat) : has_mul (matrix A n n) :=
|
||||
has_mul.mk matrix.mul
|
||||
|
||||
infix ` × ` := mul
|
||||
|
|
|
@ -21,7 +21,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
|
|||
|
||||
protected definition div := fix div.F
|
||||
|
||||
definition nat_has_divide [reducible] [instance] [priority nat.prio] : has_div nat :=
|
||||
definition nat_has_divide [instance] [priority nat.prio] : has_div nat :=
|
||||
has_div.mk nat.div
|
||||
|
||||
theorem div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
|
||||
|
@ -78,7 +78,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
|
|||
|
||||
protected definition mod := fix mod.F
|
||||
|
||||
definition nat_has_mod [reducible] [instance] [priority nat.prio] : has_mod nat :=
|
||||
definition nat_has_mod [instance] [priority nat.prio] : has_mod nat :=
|
||||
has_mod.mk nat.mod
|
||||
|
||||
notation [priority nat.prio] a ≡ b `[mod `:0 c:0 `]` := a % c = b % c
|
||||
|
|
|
@ -117,7 +117,7 @@ decidable_linear_ordered_semiring nat :=
|
|||
mul_lt_mul_of_pos_right := @nat.mul_lt_mul_of_pos_right,
|
||||
decidable_lt := nat.decidable_lt ⦄
|
||||
|
||||
definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat :=
|
||||
definition nat_has_dvd [instance] [priority nat.prio] : has_dvd nat :=
|
||||
has_dvd.mk has_dvd.dvd
|
||||
|
||||
theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
|
||||
|
|
|
@ -9,7 +9,7 @@ import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_powe
|
|||
|
||||
namespace nat
|
||||
|
||||
definition nat_has_pow_nat [instance] [reducible] [priority nat.prio] : has_pow_nat nat :=
|
||||
definition nat_has_pow_nat [instance] [priority nat.prio] : has_pow_nat nat :=
|
||||
has_pow_nat.mk has_pow_nat.pow_nat
|
||||
|
||||
theorem pow_le_pow_of_le {x y : ℕ} (i : ℕ) (H : x ≤ y) : x^i ≤ y^i :=
|
||||
|
|
|
@ -35,19 +35,19 @@ protected definition le (p q : ℕ+) := p~ ≤ q~
|
|||
|
||||
protected definition lt (p q : ℕ+) := p~ < q~
|
||||
|
||||
definition pnat_has_add [instance] [reducible] : has_add pnat :=
|
||||
definition pnat_has_add [instance] : has_add pnat :=
|
||||
has_add.mk pnat.add
|
||||
|
||||
definition pnat_has_mul [instance] [reducible] : has_mul pnat :=
|
||||
definition pnat_has_mul [instance] : has_mul pnat :=
|
||||
has_mul.mk pnat.mul
|
||||
|
||||
definition pnat_has_le [instance] [reducible] : has_le pnat :=
|
||||
definition pnat_has_le [instance] : has_le pnat :=
|
||||
has_le.mk pnat.le
|
||||
|
||||
definition pnat_has_lt [instance] [reducible] : has_lt pnat :=
|
||||
definition pnat_has_lt [instance] : has_lt pnat :=
|
||||
has_lt.mk pnat.lt
|
||||
|
||||
definition pnat_has_one [instance] [reducible] : has_one pnat :=
|
||||
definition pnat_has_one [instance] : has_one pnat :=
|
||||
has_one.mk (pos (1:nat) dec_trivial)
|
||||
|
||||
protected lemma mul_def (p q : ℕ+) : p * q = tag (p~ * q~) (mul_pos (pnat_pos p) (pnat_pos q)) :=
|
||||
|
|
|
@ -358,10 +358,10 @@ definition of_num [coercion] [reducible] (n : num) : ℚ := n
|
|||
|
||||
protected definition prio := num.pred int.prio
|
||||
|
||||
definition rat_has_zero [reducible] [instance] [priority rat.prio] : has_zero rat :=
|
||||
definition rat_has_zero [instance] [priority rat.prio] : has_zero rat :=
|
||||
has_zero.mk (of_int 0)
|
||||
|
||||
definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat :=
|
||||
definition rat_has_one [instance] [priority rat.prio] : has_one rat :=
|
||||
has_one.mk (of_int 1)
|
||||
|
||||
theorem of_int_zero : of_int (0:int) = (0:rat) :=
|
||||
|
@ -401,21 +401,21 @@ definition denom (a : ℚ) : ℤ := prerat.denom (reduce a)
|
|||
theorem denom_pos (a : ℚ): denom a > 0 :=
|
||||
prerat.denom_pos (reduce a)
|
||||
|
||||
definition rat_has_add [reducible] [instance] [priority rat.prio] : has_add rat :=
|
||||
definition rat_has_add [instance] [priority rat.prio] : has_add rat :=
|
||||
has_add.mk rat.add
|
||||
|
||||
definition rat_has_mul [reducible] [instance] [priority rat.prio] : has_mul rat :=
|
||||
definition rat_has_mul [instance] [priority rat.prio] : has_mul rat :=
|
||||
has_mul.mk rat.mul
|
||||
|
||||
definition rat_has_neg [reducible] [instance] [priority rat.prio] : has_neg rat :=
|
||||
definition rat_has_neg [instance] [priority rat.prio] : has_neg rat :=
|
||||
has_neg.mk rat.neg
|
||||
|
||||
definition rat_has_inv [reducible] [instance] [priority rat.prio] : has_inv rat :=
|
||||
definition rat_has_inv [instance] [priority rat.prio] : has_inv rat :=
|
||||
has_inv.mk rat.inv
|
||||
|
||||
protected definition sub [reducible] (a b : ℚ) : rat := a + (-b)
|
||||
|
||||
definition rat_has_sub [reducible] [instance] [priority rat.prio] : has_sub rat :=
|
||||
definition rat_has_sub [instance] [priority rat.prio] : has_sub rat :=
|
||||
has_sub.mk rat.sub
|
||||
|
||||
lemma sub.def (a b : ℚ) : a - b = a + (-b) :=
|
||||
|
@ -574,10 +574,10 @@ protected definition discrete_field [reducible] [trans_instance] : discrete_fiel
|
|||
inv_zero := rat.inv_zero,
|
||||
has_decidable_eq := has_decidable_eq⦄
|
||||
|
||||
definition rat_has_div [instance] [reducible] [priority rat.prio] : has_div rat :=
|
||||
definition rat_has_div [instance] [priority rat.prio] : has_div rat :=
|
||||
has_div.mk has_div.div
|
||||
|
||||
definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat :=
|
||||
definition rat_has_pow_nat [instance] [priority rat.prio] : has_pow_nat rat :=
|
||||
has_pow_nat.mk has_pow_nat.pow_nat
|
||||
|
||||
theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
|
||||
|
|
|
@ -142,10 +142,10 @@ quot.rec_on_subsingleton a (take u, int.decidable_lt 0 (prerat.num u))
|
|||
protected definition lt (a b : ℚ) : Prop := pos (b - a)
|
||||
protected definition le (a b : ℚ) : Prop := nonneg (b - a)
|
||||
|
||||
definition rat_has_lt [reducible] [instance] [priority rat.prio] : has_lt rat :=
|
||||
definition rat_has_lt [instance] [priority rat.prio] : has_lt rat :=
|
||||
has_lt.mk rat.lt
|
||||
|
||||
definition rat_has_le [reducible] [instance] [priority rat.prio] : has_le rat :=
|
||||
definition rat_has_le [instance] [priority rat.prio] : has_le rat :=
|
||||
has_le.mk rat.le
|
||||
|
||||
protected lemma lt_def (a b : ℚ) : (a < b) = pos (b - a) :=
|
||||
|
|
|
@ -1075,18 +1075,18 @@ protected definition neg (x : ℝ) : ℝ :=
|
|||
quot.sound (rneg_well_defined Hab)))
|
||||
--prefix [priority real.prio] `-` := neg
|
||||
|
||||
definition real_has_add [reducible] [instance] [priority real.prio] : has_add real :=
|
||||
definition real_has_add [instance] [priority real.prio] : has_add real :=
|
||||
has_add.mk real.add
|
||||
|
||||
definition real_has_mul [reducible] [instance] [priority real.prio] : has_mul real :=
|
||||
definition real_has_mul [instance] [priority real.prio] : has_mul real :=
|
||||
has_mul.mk real.mul
|
||||
|
||||
definition real_has_neg [reducible] [instance] [priority real.prio] : has_neg real :=
|
||||
definition real_has_neg [instance] [priority real.prio] : has_neg real :=
|
||||
has_neg.mk real.neg
|
||||
|
||||
protected definition sub [reducible] (a b : ℝ) : real := a + (-b)
|
||||
|
||||
definition real_has_sub [reducible] [instance] [priority real.prio] : has_sub real :=
|
||||
definition real_has_sub [instance] [priority real.prio] : has_sub real :=
|
||||
has_sub.mk real.sub
|
||||
|
||||
open rat -- no coercions before
|
||||
|
|
|
@ -587,7 +587,7 @@ noncomputable protected definition inv (x : ℝ) : ℝ :=
|
|||
quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a))
|
||||
(λ a b H, quot.sound (rat_seq.r_inv_well_defined H))
|
||||
|
||||
noncomputable definition real_has_inv [instance] [reducible] [priority real.prio] : has_inv real :=
|
||||
noncomputable definition real_has_inv [instance] [priority real.prio] : has_inv real :=
|
||||
has_inv.mk real.inv
|
||||
|
||||
noncomputable protected definition div (x y : ℝ) : ℝ :=
|
||||
|
@ -596,7 +596,7 @@ noncomputable protected definition div (x y : ℝ) : ℝ :=
|
|||
noncomputable definition real_has_div : has_div real :=
|
||||
has_div.mk real.div
|
||||
|
||||
local attribute real_has_div [instance] [reducible] [priority real.prio]
|
||||
local attribute real_has_div [instance] [priority real.prio]
|
||||
|
||||
protected theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
|
||||
quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t)
|
||||
|
|
|
@ -1026,10 +1026,10 @@ protected definition lt (x y : ℝ) :=
|
|||
protected definition le (x y : ℝ) :=
|
||||
quot.lift_on₂ x y (λ a b, rat_seq.r_le a b) rat_seq.r_le_well_defined
|
||||
|
||||
definition real_has_lt [reducible] [instance] [priority real.prio] : has_lt ℝ :=
|
||||
definition real_has_lt [instance] [priority real.prio] : has_lt ℝ :=
|
||||
has_lt.mk real.lt
|
||||
|
||||
definition real_has_le [reducible] [instance] [priority real.prio] : has_le ℝ :=
|
||||
definition real_has_le [instance] [priority real.prio] : has_le ℝ :=
|
||||
has_le.mk real.le
|
||||
|
||||
definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_sep a b) rat_seq.r_sep_well_defined
|
||||
|
|
|
@ -39,13 +39,13 @@ namespace nat
|
|||
| nat_refl : le a a -- use nat_refl to avoid overloading le.refl
|
||||
| step : Π {b}, le a b → le a (succ b)
|
||||
|
||||
definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
definition nat_has_le [instance] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
|
||||
protected lemma le_refl [refl] : ∀ a : nat, a ≤ a :=
|
||||
le.nat_refl
|
||||
|
||||
protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
definition nat_has_lt [instance] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
|
||||
definition pred [unfold 1] (a : nat) : nat :=
|
||||
nat.cases_on a zero (λ a₁, a₁)
|
||||
|
@ -58,10 +58,10 @@ namespace nat
|
|||
protected definition mul (a b : nat) : nat :=
|
||||
nat.rec_on b zero (λ b₁ r, r + a)
|
||||
|
||||
definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat :=
|
||||
definition nat_has_sub [instance] [priority nat.prio] : has_sub nat :=
|
||||
has_sub.mk nat.sub
|
||||
|
||||
definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat :=
|
||||
definition nat_has_mul [instance] [priority nat.prio] : has_mul nat :=
|
||||
has_mul.mk nat.mul
|
||||
|
||||
/- properties of ℕ -/
|
||||
|
|
|
@ -34,7 +34,7 @@ namespace pos_num
|
|||
pos_num.lt a (succ b)
|
||||
end pos_num
|
||||
|
||||
definition pos_num_has_mul [instance] [reducible] : has_mul pos_num :=
|
||||
definition pos_num_has_mul [instance] : has_mul pos_num :=
|
||||
has_mul.mk pos_num.mul
|
||||
|
||||
namespace num
|
||||
|
@ -50,7 +50,7 @@ namespace num
|
|||
num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
|
||||
end num
|
||||
|
||||
definition num_has_mul [instance] [reducible] : has_mul num :=
|
||||
definition num_has_mul [instance] : has_mul num :=
|
||||
has_mul.mk num.mul
|
||||
|
||||
namespace num
|
||||
|
@ -80,5 +80,5 @@ namespace num
|
|||
num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
|
||||
end num
|
||||
|
||||
definition num_has_sub [instance] [reducible] : has_sub num :=
|
||||
definition num_has_sub [instance] : has_sub num :=
|
||||
has_sub.mk num.sub
|
||||
|
|
|
@ -40,13 +40,13 @@ definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a
|
|||
definition bit0 {A : Type} [s : has_add A] (a : A) : A := add a a
|
||||
definition bit1 {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one
|
||||
|
||||
definition num_has_zero [reducible] [instance] : has_zero num :=
|
||||
definition num_has_zero [instance] : has_zero num :=
|
||||
has_zero.mk num.zero
|
||||
|
||||
definition num_has_one [reducible] [instance] : has_one num :=
|
||||
definition num_has_one [instance] : has_one num :=
|
||||
has_one.mk (num.pos pos_num.one)
|
||||
|
||||
definition pos_num_has_one [reducible] [instance] : has_one pos_num :=
|
||||
definition pos_num_has_one [instance] : has_one pos_num :=
|
||||
has_one.mk (pos_num.one)
|
||||
|
||||
namespace pos_num
|
||||
|
@ -74,7 +74,7 @@ namespace pos_num
|
|||
b
|
||||
end pos_num
|
||||
|
||||
definition pos_num_has_add [reducible] [instance] : has_add pos_num :=
|
||||
definition pos_num_has_add [instance] : has_add pos_num :=
|
||||
has_add.mk pos_num.add
|
||||
|
||||
namespace num
|
||||
|
@ -84,7 +84,7 @@ namespace num
|
|||
num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
|
||||
end num
|
||||
|
||||
definition num_has_add [reducible] [instance] : has_add num :=
|
||||
definition num_has_add [instance] : has_add num :=
|
||||
has_add.mk num.add
|
||||
|
||||
definition std.priority.default : num := 1000
|
||||
|
@ -104,13 +104,13 @@ end nat
|
|||
attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
|
||||
[instance] [priority nat.prio]
|
||||
|
||||
definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
|
||||
definition nat_has_zero [instance] [priority nat.prio] : has_zero nat :=
|
||||
has_zero.mk nat.zero
|
||||
|
||||
definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
|
||||
definition nat_has_one [instance] [priority nat.prio] : has_one nat :=
|
||||
has_one.mk (nat.succ (nat.zero))
|
||||
|
||||
definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
|
||||
definition nat_has_add [instance] [priority nat.prio] : has_add nat :=
|
||||
has_add.mk nat.add
|
||||
|
||||
/-
|
||||
|
|
|
@ -31,10 +31,10 @@ protected definition prio := num.pred real.prio
|
|||
|
||||
/- arithmetic operations on the ereals -/
|
||||
|
||||
definition ereal_has_zero [reducible] [instance] [priority ereal.prio] : has_zero ereal :=
|
||||
definition ereal_has_zero [instance] [priority ereal.prio] : has_zero ereal :=
|
||||
has_zero.mk (of_real 0)
|
||||
|
||||
definition ereal_has_one [reducible] [instance] [priority ereal.prio] : has_one ereal :=
|
||||
definition ereal_has_one [instance] [priority ereal.prio] : has_one ereal :=
|
||||
has_one.mk (of_real 1)
|
||||
|
||||
protected definition add : ereal → ereal → ereal
|
||||
|
@ -61,18 +61,18 @@ protected definition mul : ereal → ereal → ereal
|
|||
| -∞ a := ereal.neg (blow_up a)
|
||||
| a -∞ := ereal.neg (blow_up a)
|
||||
|
||||
definition ereal_has_add [reducible] [instance] [priority ereal.prio] : has_add ereal :=
|
||||
definition ereal_has_add [instance] [priority ereal.prio] : has_add ereal :=
|
||||
has_add.mk ereal.add
|
||||
|
||||
definition ereal_has_neg [reducible] [instance] [priority ereal.prio] : has_neg ereal :=
|
||||
definition ereal_has_neg [instance] [priority ereal.prio] : has_neg ereal :=
|
||||
has_neg.mk ereal.neg
|
||||
|
||||
protected definition sub (u v : ereal) : ereal := u + -v
|
||||
|
||||
definition ereal_has_sub [reducible] [instance] [priority ereal.prio] : has_sub ereal :=
|
||||
definition ereal_has_sub [instance] [priority ereal.prio] : has_sub ereal :=
|
||||
has_sub.mk ereal.sub
|
||||
|
||||
definition ereal_has_mul [reducible] [instance] [priority ereal.prio] : has_mul ereal :=
|
||||
definition ereal_has_mul [instance] [priority ereal.prio] : has_mul ereal :=
|
||||
has_mul.mk ereal.mul
|
||||
|
||||
protected theorem zero_def : (0 : ereal) = of_real 0 := rfl
|
||||
|
@ -313,7 +313,7 @@ protected definition le : ereal → ereal → Prop
|
|||
| ∞ (of_real y) := false
|
||||
| ∞ -∞ := false
|
||||
|
||||
definition ereal_has_le [reducible] [instance] [priority ereal.prio] :
|
||||
definition ereal_has_le [instance] [priority ereal.prio] :
|
||||
has_le ereal :=
|
||||
has_le.mk ereal.le
|
||||
|
||||
|
@ -362,7 +362,7 @@ protected theorem le_antisymm : ∀ u v : ereal, u ≤ v → v ≤ u → u = v
|
|||
|
||||
protected definition lt (x y : ereal) : Prop := x ≤ y ∧ x ≠ y
|
||||
|
||||
definition ereal_has_lt [reducible] [instance] [priority ereal.prio] :
|
||||
definition ereal_has_lt [instance] [priority ereal.prio] :
|
||||
has_lt ereal :=
|
||||
has_lt.mk ereal.lt
|
||||
|
||||
|
|
|
@ -112,7 +112,7 @@ theorem measurable_generated_by {G : set (set X)} :
|
|||
|
||||
protected definition le (M N : sigma_algebra X) : Prop := @sets _ M ⊆ @sets _ N
|
||||
|
||||
definition sigma_algebra_has_le [reducible] [instance] :
|
||||
definition sigma_algebra_has_le [instance] :
|
||||
has_le (sigma_algebra X) :=
|
||||
has_le.mk sigma_algebra.le
|
||||
|
||||
|
|
|
@ -157,8 +157,8 @@ namespace topology
|
|||
(T0_space.T0)
|
||||
(assume H, obtain U [OpU xyU], from H,
|
||||
suppose x = y,
|
||||
have x ∈ U ↔ y ∈ U, from iff.intro
|
||||
(assume xU, this ▸ xU)
|
||||
have x ∈ U ↔ y ∈ U, from iff.intro
|
||||
(assume xU, this ▸ xU)
|
||||
(assume yU, this⁻¹ ▸ yU),
|
||||
absurd this xyU)
|
||||
end topology
|
||||
|
@ -179,16 +179,16 @@ protected definition T0_space.of_T1 [reducible] [trans_instance] {X : Type} [T :
|
|||
namespace topology
|
||||
variables {X : Type} [T1_space X]
|
||||
|
||||
theorem separation_T1 {x y : X} : x ≠ y ↔ (∃ U, Open U ∧ x ∈ U ∧ y ∉ U) :=
|
||||
theorem separation_T1 {x y : X} : x ≠ y ↔ (∃ U, Open U ∧ x ∈ U ∧ y ∉ U) :=
|
||||
iff.intro
|
||||
(T1_space.T1)
|
||||
(suppose ∃ U, Open U ∧ x ∈ U ∧ y ∉ U,
|
||||
(suppose ∃ U, Open U ∧ x ∈ U ∧ y ∉ U,
|
||||
obtain U [OpU xU nyU], from this,
|
||||
suppose x = y,
|
||||
suppose x = y,
|
||||
absurd xU (this⁻¹ ▸ nyU))
|
||||
|
||||
theorem closed_singleton {a : X} : closed '{a} :=
|
||||
let T := ⋃₀ {S| Open S ∧ a ∉ S} in
|
||||
|
||||
theorem closed_singleton {a : X} : closed '{a} :=
|
||||
let T := ⋃₀ {S| Open S ∧ a ∉ S} in
|
||||
have Open T, from Open_sUnion (λS HS, and.elim_left HS),
|
||||
have T = -'{a}, from ext(take x, iff.intro
|
||||
(assume xT, assume xa,
|
||||
|
@ -197,7 +197,7 @@ namespace topology
|
|||
exists.intro S (and.intro OpS (and.intro xS aS)),
|
||||
have x ≠ a, from (iff.elim_right separation_T1) this,
|
||||
absurd ((iff.elim_left !mem_singleton_iff) xa) this)
|
||||
(assume xa,
|
||||
(assume xa,
|
||||
have x ≠ a, from not.intro(
|
||||
assume H, absurd ((iff.elim_right !mem_singleton_iff) H) xa),
|
||||
obtain U [OpU xU aU], from (iff.elim_left separation_T1) this,
|
||||
|
@ -223,10 +223,10 @@ protected definition T1_space.of_T2 [reducible] [trans_instance] {X : Type} [T :
|
|||
namespace topology
|
||||
variables {X : Type} [T2_space X]
|
||||
|
||||
theorem seperation_T2 {x y : X} : x ≠ y ↔ ∃ U V, Open U ∧ Open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅ :=
|
||||
theorem seperation_T2 {x y : X} : x ≠ y ↔ ∃ U V, Open U ∧ Open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅ :=
|
||||
iff.intro
|
||||
(T2_space.T2)
|
||||
(assume H, obtain U V [OpU OpV xU yV UV], from H,
|
||||
(assume H, obtain U V [OpU OpV xU yV UV], from H,
|
||||
suppose x = y,
|
||||
have ¬(x ∈ U ∩ V), from not.intro(
|
||||
assume xUV, absurd (UV ▸ xUV) !not_mem_empty),
|
||||
|
@ -247,7 +247,7 @@ inductive opens_generated_by {X : Type} (B : set (set X)) : set X → Prop :=
|
|||
opens_generated_by B (s ∩ t)
|
||||
| sUnion_mem : ∀ ⦃S : set (set X)⦄, S ⊆ opens_generated_by B → opens_generated_by B (⋃₀ S)
|
||||
|
||||
protected definition generated_by [instance] [reducible] {X : Type} (B : set (set X)) : topology X :=
|
||||
protected definition generated_by [instance] {X : Type} (B : set (set X)) : topology X :=
|
||||
⦃topology,
|
||||
opens := opens_generated_by B,
|
||||
univ_mem_opens := opens_generated_by.univ_mem B,
|
||||
|
|
|
@ -14,7 +14,7 @@ variables {X : Type} [linear_strong_order_pair X]
|
|||
|
||||
definition linorder_generators : set (set X) := {y | ∃ a, y = '(a, ∞) } ∪ {y | ∃ a, y = '(-∞, a)}
|
||||
|
||||
definition linorder_topology [instance] [reducible] : topology X :=
|
||||
definition linorder_topology [instance] : topology X :=
|
||||
topology.generated_by linorder_generators
|
||||
|
||||
theorem Open_Ioi {a : X} : Open '(a, ∞) :=
|
||||
|
|
Loading…
Reference in a new issue