feat(data/ordinal): is_normal, omin, power/log, CNF, indecomposables,

addition and multiplication of infinite cardinals

algebra/linear_algebra/basic.lean

@@ -179,9 +179,9 @@ span_eq is_submodule_span (set.insert_subset.mpr ⟨h, subset_span⟩) (span_mon
 lemma span_insert : span (insert b s) = {z | ∃a, ∃x∈span s, z = a • b + x } :=
 set.ext $ assume b',
 begin
-  apply iff.intro; simp [insert_eq, span_union, span_singleton, set.set_eq_def, range],
-  exact (assume x hx y a eq_y eq, ⟨a, x, hx, by simp [eq_y, eq]⟩),
-  exact (assume a b₂ hb₂ eq, ⟨b₂, hb₂, a • b, ⟨a, rfl⟩, eq⟩)
+  apply iff.intro; simp [insert_eq, span_union, span_singleton, set.set_eq_def, range, -add_comm],
+  exact (assume y a eq_y x hx eq, ⟨a, x, hx, by simp [eq_y, eq]⟩),
+  exact (assume a b₂ hb₂ eq, ⟨a • b, ⟨a, rfl⟩, b₂, hb₂, eq⟩)
 end
 
 lemma mem_span_insert : b₁ ∈ span (insert b s) ↔ ∃a, b₁ + a • b ∈ span s :=

algebra/module.lean

@@ -213,7 +213,7 @@ instance sInter_submodule {s : set (set β)} [hs : ∀t∈s, is_submodule t] : i
 by rw [set.sInter_eq_Inter]; exact Inter_submodule (assume t, Inter_submodule $ hs t)
 
 instance inter_submodule : is_submodule (p ∩ p') :=
-suffices is_submodule (⋂₀ {p, p'} : set β), by simpa,
+suffices is_submodule (⋂₀ {p, p'} : set β), by simpa [set.inter_comm],
 @is_submodule.sInter_submodule α β _ _ {p, p'} $
   by simp [or_imp_distrib, ‹is_submodule p›, ‹is_submodule p'›] {contextual := tt}
 

algebra/order.lean

@@ -34,6 +34,12 @@ lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ a > b := le_or_gt
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl
 
+lemma lt_iff_lt_of_strict_mono {β} [linear_order α] [linear_order β]
+  (f : α → β) (H : ∀ a b, a < b → f a < f b) {a b} :
+  f a < f b ↔ a < b :=
+⟨by rw [← not_le, ← not_le, le_iff_lt_or_eq, le_iff_lt_or_eq];
+    exact mt (or.imp (H _ _) (congr_arg _)), H _ _⟩
+
 lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [linear_order β] {a b : α} {c d : β} :
   (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
 ⟨λ H h, lt_of_not_ge $ λ h', not_lt_of_ge (H h') h,

analysis/measure_theory/measurable_space.lean

@@ -460,7 +460,7 @@ have hf2 : ∀n:ℕ, f n.succ.succ = ∅, from assume n, rfl,
 have (∀i j, i ≠ j → f i ∩ f j = ∅),
   from assume i, i.two_step_induction
     (assume j, j.two_step_induction (by simp) (by simp [hf0, hf1, h]) (by simp [hf2]))
-    (assume j, j.two_step_induction (by simp [hf0, hf1, h]) (by simp) (by simp [hf2]))
+    (assume j, j.two_step_induction (by simp [hf0, hf1, h, inter_comm]) (by simp) (by simp [hf2]))
     (by simp [hf2]),
 have eq : s₁ ∪ s₂ = (⋃i, f i),
   from subset.antisymm (union_subset (le_supr f 0) (le_supr f 1)) $

analysis/measure_theory/measure_space.lean

@@ -280,7 +280,7 @@ lemma measure_Union_eq_supr_nat {s : ℕ → set α} (h : ∀i, is_measurable (s
 have ∀i, (range (i + 1)).sum (λi, μ.measure (disjointed s i)) = μ.measure (s i),
 begin
   intro i, induction i,
-  case nat.zero { simp [disjointed, nat.not_lt_zero, univ_inter] },
+  case nat.zero { simp [disjointed, nat.not_lt_zero, inter_univ] },
   case nat.succ : i ih {
     rw [range_succ, sum_insert, ih, ←measure_union],
     { show μ.measure (disjointed s (i + 1) ∪ s i) = μ.measure (s (i + 1)),

analysis/measure_theory/outer_measure.lean

@@ -121,6 +121,7 @@ parameters {α : Type u} (m : outer_measure α)
 include m
 
 local notation `μ` := m.measure_of
+local attribute [simp] set.inter_comm set.inter_left_comm set.inter_assoc
 
 variables {s s₁ s₂ : set α}
 

analysis/topology/topological_space.lean

@@ -58,7 +58,7 @@ end
 variables [topological_space α]
 
 lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
-have (⋃₀ {s₁, s₂}) = (s₁ ∪ s₂), by simp,
+have (⋃₀ {s₁, s₂}) = (s₁ ∪ s₂), by simp [union_comm],
 this ▸ is_open_sUnion $ show ∀(t : set α), t ∈ ({s₁, s₂} : set (set α)) → is_open t,
   by finish
 
@@ -355,9 +355,9 @@ have nhds a ⊓ principal (s ∩ t) ≠ ⊥,
 by rw [closure_eq_nhds]; assumption
 
 lemma closure_diff {s t : set α} : closure s - closure t ⊆ closure (s - t) :=
-calc closure s \ closure t = (- closure t) ∩ closure s : by simp [diff_eq]
+calc closure s \ closure t = (- closure t) ∩ closure s : by simp [diff_eq, inter_comm]
   ... ⊆ closure (- closure t ∩ s) : closure_inter_open $ is_open_compl_iff.mpr $ is_closed_closure
-  ... = closure (s \ closure t) : by simp [diff_eq]
+  ... = closure (s \ closure t) : by simp [diff_eq, inter_comm]
   ... ⊆ closure (s \ t) : closure_mono $ diff_subset_diff (subset.refl s) subset_closure
 
 lemma mem_of_closed_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
@@ -409,7 +409,7 @@ is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
     simp,
     intro x,
     simp [not_eq_empty_iff_exists],
-    exact assume xt ht i xfi, ht i x xt xfi xfi
+    exact assume xt ht i xfi, ht i x xfi xt xfi
   end
 
 end locally_finite

analysis/topology/topological_structures.lean

@@ -346,7 +346,7 @@ calc nhds a = (⨅b<a, principal {c | b < c}) ⊓ (⨅b>a, principal {c | c < b}
       rw [inf_comm],
       apply binfi_inf hu
     end
-  ... = _ : by simp; refl
+  ... = _ : by simp [inter_comm]; refl
 
 lemma tendsto_orderable_unbounded {f : β → α} {a : α} {x : filter β}
   (hu : ∃u, a < u) (hl : ∃l, l < a) (h : ∀l u, l < a → a < u → {b | l < f b ∧ f b < u } ∈ x.sets) :
@@ -683,7 +683,7 @@ begin
       exact lt_of_add_lt_add_right this } },
   { have h : {b | abs (a + -b) < r} = {b | a - r < b} ∩ {b | b < a + r},
       from set.ext (assume b,
-        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm, sub_lt, lt_sub_iff]),
+        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm, sub_lt, lt_sub_iff, and_comm]),
     rw [h, ← inf_principal],
     apply le_inf _ _,
     { exact infi_le_of_le {b : α | a - r < b} (infi_le_of_le (sub_lt_self a hr) $

analysis/topology/uniform_space.lean

@@ -625,7 +625,7 @@ instance separated_regular [separated α] : regular_space α :=
     have closure e ∈ (nhds a).sets, from (nhds a).upwards_sets (mem_nhds_left hd) subset_closure,
     have nhds a ⊓ principal (-closure e) = ⊥,
       from (@inf_eq_bot_iff_le_compl _ _ _ (principal (- closure e)) (principal (closure e))
-        (by simp [principal_univ]) (by simp)).mpr (by simp [this]),
+        (by simp [principal_univ, union_comm]) (by simp)).mpr (by simp [this]),
     ⟨- closure e, is_closed_closure, assume x h₁ h₂, @e_subset x h₂ h₁, this⟩,
   ..separated_t2 }
 
@@ -1114,7 +1114,7 @@ have h_ex : ∀s∈(@uniformity (Cauchy α) _).sets, ∃y:α, (f, pure_cauchy y)
         ht'₂ $ prod_mk_mem_comp_rel (@h (a, x) ⟨h₁, hx⟩) h₂⟩,
   ⟨x, ht''₂ $ by dsimp [gen]; exact this⟩,
 begin
-  simp [closure_eq_nhds, nhds_eq_uniformity, lift'_inf_principal_eq],
+  simp [closure_eq_nhds, nhds_eq_uniformity, lift'_inf_principal_eq, set.inter_comm],
   exact (lift'_neq_bot_iff $ monotone_inter monotone_const monotone_preimage).mpr
     (assume s hs,
       let ⟨y, hy⟩ := h_ex s hs in

data/cardinal.lean

@@ -5,11 +5,7 @@ Author: Johannes Hölzl, Mario Carneiro
 
 Cardinal arithmetic.
 
-Cardinals are represented as quotient over equinumerable types.
-
-Future work:
-* define ordinal numbers and relate them to cardinals
-* proof `κ + κ = κ` and `κ * κ = κ` for all infinite cardinal `κ`
+Cardinals are represented as quotient over equinumerous types.
 -/
 
 import data.set.finite data.quot logic.schroeder_bernstein logic.function
@@ -177,46 +173,64 @@ from (quotient.induction_on₃ a b c $ assume α β γ,
 section order_properties
 open sum
 
-theorem zero_le (a : cardinal.{u}) : 0 ≤ a :=
+theorem zero_le (a : cardinal) : 0 ≤ a :=
 quot.induction_on a $ λ α, ⟨embedding.of_not_nonempty $ λ ⟨⟨a⟩⟩, a.elim⟩
 
-theorem le_zero (a : cardinal.{u}) : a ≤ 0 ↔ a = 0 :=
+theorem le_zero (a : cardinal) : a ≤ 0 ↔ a = 0 :=
 by simp [le_antisymm_iff, zero_le]
 
 theorem zero_lt_one : (0 : cardinal) < 1 :=
 lt_of_le_of_ne (zero_le _) zero_ne_one
 
-theorem add_mono {a b c d : cardinal.{u}} : a ≤ b → c ≤ d → a + c ≤ b + d :=
+theorem add_le_add {a b c d : cardinal} : a ≤ b → c ≤ d → a + c ≤ b + d :=
 quotient.induction_on₂ a b $ assume α β, quotient.induction_on₂ c d $ assume γ δ ⟨e₁⟩ ⟨e₂⟩,
   ⟨embedding.sum_congr e₁ e₂⟩
 
-theorem mul_mono {a b c d : cardinal.{u}} : a ≤ b → c ≤ d → a * c ≤ b * d :=
+theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
+add_le_add (le_refl _)
+
+theorem add_le_add_right {a b : cardinal} (c) (h : a ≤ b) : a + c ≤ b + c :=
+add_le_add h (le_refl _)
+
+theorem le_add_right (a b : cardinal) : a ≤ a + b :=
+by simpa using add_le_add_left a (zero_le b)
+
+theorem le_add_left (a b : cardinal) : a ≤ b + a :=
+by simpa using add_le_add_right a (zero_le b)
+
+theorem mul_le_mul {a b c d : cardinal} : a ≤ b → c ≤ d → a * c ≤ b * d :=
 quotient.induction_on₂ a b $ assume α β, quotient.induction_on₂ c d $ assume γ δ ⟨e₁⟩ ⟨e₂⟩,
   ⟨embedding.prod_congr e₁ e₂⟩
 
-theorem power_mono_left {a b c : cardinal.{u}} : a ≤ b → a ^ c ≤ b ^ c :=
-quotient.induction_on₃ a b c $ assume α β γ ⟨e⟩, ⟨embedding.arrow_congr_left e⟩
+theorem mul_le_mul_left (a) {b c : cardinal} : b ≤ c → a * b ≤ a * c :=
+mul_le_mul (le_refl _)
 
-theorem power_mono_right {a b c : cardinal.{u}} : a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
+theorem mul_le_mul_right {a b : cardinal} (c) (h : a ≤ b) : a * c ≤ b * c :=
+mul_le_mul h (le_refl _)
+
+theorem power_le_power_left {a b c : cardinal} : a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
 quotient.induction_on₃ a b c $ assume α β γ hα ⟨e⟩,
   have nonempty α, from classical.by_contradiction $ assume hnα,
     hα $ quotient.sound ⟨equiv.trans (equiv.empty_of_not_nonempty hnα) equiv.ulift.symm⟩,
   let ⟨a⟩ := this in
   ⟨@embedding.arrow_congr_right _ _ _ ⟨a⟩ e⟩
 
-theorem le_iff_exists_add {a b : cardinal.{u}} : a ≤ b ↔ ∃ c, b = a + c :=
+theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
+quotient.induction_on₃ a b c $ assume α β γ ⟨e⟩, ⟨embedding.arrow_congr_left e⟩
+
+theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
 ⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
   have (α ⊕ ↥-range f) ≃ β, from
     (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
     (equiv.set.sum_compl (range f)),
   ⟨⟦(-range f : set β)⟧, quotient.sound ⟨this.symm⟩⟩,
- λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ add_mono (le_refl _) (zero_le _)⟩
+ λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ add_le_add_left _ (zero_le _)⟩
 
 end order_properties
 
 instance : canonically_ordered_monoid cardinal.{u} :=
-{ add_le_add_left       := λ a b h c, add_mono (le_refl _) h,
-  lt_of_add_lt_add_left := λ a b c, le_imp_le_iff_lt_imp_lt.1 (add_mono (le_refl _)),
+{ add_le_add_left       := λ a b h c, add_le_add_left _ h,
+  lt_of_add_lt_add_left := λ a b c, le_imp_le_iff_lt_imp_lt.1 (add_le_add_left _),
   le_iff_exists_add     := @le_iff_exists_add,
   ..cardinal.comm_semiring, ..cardinal.linear_order }
 
@@ -435,6 +449,9 @@ theorem nat_lt_omega (n : ℕ) : (n : cardinal.{u}) < omega :=
 succ_le.1 $ by rw [nat_succ, ← lift_mk_fin, omega, lift_mk_le.{0 0 u}]; exact
 ⟨⟨fin.val, λ a b, fin.eq_of_veq⟩⟩
 
+theorem one_lt_omega : 1 < omega :=
+by simpa using nat_lt_omega 1
+
 theorem lt_omega {c : cardinal.{u}} : c < omega ↔ ∃ n : ℕ, c = n :=
 ⟨λ h, begin
   rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩,
@@ -464,6 +481,13 @@ theorem lt_omega {c : cardinal.{u}} : c < omega ↔ ∃ n : ℕ, c = n :=
   exact λ e, this ⟨m, h, e⟩,
 end, λ ⟨n, e⟩, e.symm ▸ nat_lt_omega _⟩
 
+theorem omega_le {c : cardinal.{u}} : omega ≤ c ↔ ∀ n : ℕ, (n:cardinal) ≤ c :=
+⟨λ h n, le_trans (le_of_lt (nat_lt_omega _)) h,
+ λ h, le_of_not_lt $ λ hn, begin
+  rcases lt_omega.1 hn with ⟨n, rfl⟩,
+  exact not_le_of_lt (nat.lt_succ_self _) (nat_cast_le.1 (h (n+1)))
+end⟩
+
 theorem lt_omega_iff_fintype {α : Type u} : mk α < omega ↔ nonempty (fintype α) :=
 lt_omega.trans ⟨λ ⟨n, e⟩, begin
   rw [← lift_mk_fin n] at e,
@@ -474,4 +498,14 @@ end, λ ⟨_⟩, by exact ⟨_, fintype_card _⟩⟩
 theorem lt_omega_iff_finite {α} {S : set α} : mk S < omega ↔ finite S :=
 lt_omega_iff_fintype
 
+theorem add_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a + b < omega :=
+match a, b, lt_omega.1 ha, lt_omega.1 hb with
+| _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_add]; apply nat_lt_omega
+end
+
+theorem mul_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a * b < omega :=
+match a, b, lt_omega.1 ha, lt_omega.1 hb with
+| _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_mul]; apply nat_lt_omega
+end
+
 end cardinal

data/equiv.lean

@@ -475,6 +475,17 @@ protected def union {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅) :
  λ o, by rcases o with ⟨x, h⟩ | ⟨x, h⟩; simp [union._match_1, union._match_2, h];
    simp [show x ∉ s, from λ h', eq_empty_iff_forall_not_mem.1 H _ ⟨h', h⟩]⟩
 
+protected def singleton {α} (a : α) : ({a} : set α) ≃ unit :=
+⟨λ _, (), λ _, ⟨a, mem_singleton _⟩,
+ λ ⟨x, h⟩, by simp at h; subst x,
+ λ ⟨⟩, rfl⟩
+
+protected def insert {α} {s : set.{u} α} [decidable_pred s] {a : α} (H : a ∉ s) :
+  (insert a s : set α) ≃ (s ⊕ unit) :=
+by rw ← union_singleton; exact
+(set.union $ inter_singleton_eq_empty.2 H).trans
+  (sum_congr (equiv.refl _) (set.singleton _))
+
 protected def sum_compl {α} (s : set α) [decidable_pred s] :
   (s ⊕ (-s : set α)) ≃ α :=
 (set.union (inter_compl_self _)).symm.trans