feat(data/dardinal): wellordering of cardinals

Author: digama0

algebra/linear_algebra/basic.lean

@@ -607,10 +607,15 @@ have t ⊆ span m,
   hbm this,
 ⟨m, hmt, hsm, this, hml⟩
 
-lemma exists_is_basis (hs : linear_independent s) : ∃b, s ⊆ b ∧ is_basis b :=
+lemma exists_subset_is_basis (hs : linear_independent s) : ∃b, s ⊆ b ∧ is_basis b :=
 let ⟨b, hb₀, hb₁, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_univ _ _) in
 ⟨b, hb₁, hb₃, assume x, hb₂ trivial⟩
 
+variable (β)
+lemma exists_is_basis : ∃b : set β, is_basis b :=
+let ⟨b, _, hb⟩ := exists_subset_is_basis linear_independent_empty in ⟨b, hb⟩
+variable {β}
+
 lemma eq_of_linear_independent_of_span
   (hs : linear_independent s) (h : t ⊆ s) (hst : s ⊆ span t) : s = t :=
 suffices s ⊆ t, from subset.antisymm this h,
@@ -679,10 +684,10 @@ have finite s, from finite_subset u.finite_to_set hsu,
 
 lemma exists_left_inverse_linear_map_of_injective {f : β → γ}
   (hf : is_linear_map f) (hf_inj : injective f) : ∃g:γ → β, is_linear_map g ∧ g ∘ f = id :=
-let ⟨bβ, _, hbβ⟩ := exists_is_basis linear_independent_empty in
+let ⟨bβ, hbβ⟩ := exists_is_basis β in
 have linear_independent (f '' bβ),
   from hbβ.1.image hf $ assume b₁ _ b₂ _ eq, hf_inj eq,
-let ⟨bγ, hbγ₁, hbγ₂⟩ := exists_is_basis this in
+let ⟨bγ, hbγ₁, hbγ₂⟩ := exists_subset_is_basis this in
 have ∀b∈bβ, (hbγ₂.constr (@inv_fun _ _ ⟨0⟩ f) : γ → β) (f b) = b,
   begin
     assume b hb,
@@ -699,7 +704,7 @@ lemma exists_right_inverse_linear_map_of_surjective {f : β → γ}
 let g := @inv_fun _ _ ⟨0⟩ f in
 have ri_gf : right_inverse g f, from @right_inverse_inv_fun _ _ _ ⟨0⟩ hf_surj,
 have injective g, from injective_of_left_inverse ri_gf,
-let ⟨bγ, _, hbγ⟩ := exists_is_basis (linear_independent_empty : linear_independent (∅ : set γ)) in
+let ⟨bγ, hbγ⟩ := exists_is_basis γ in
 have ∀c∈bγ, f ((hbγ.constr g : γ → β) c) = c,
   from assume c hc, by rw [constr_basis hbγ hc, ri_gf],
 ⟨hbγ.constr g, hbγ.map_constr, hbγ.eq_linear_map (hf.comp hbγ.map_constr) is_linear_map.id this⟩

analysis/measure_theory/measurable_space.lean

@@ -479,7 +479,7 @@ by rw [eq]; exact d.has_Union this (assume i,
 
 lemma has_sdiff {s₁ s₂ : set δ} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ ⊆ s₁) : d.has (s₁ - s₂) :=
 have d.has (- (s₂ ∪ -s₁)),
-  from d.has_compl $ d.has_union h₂ (d.has_compl h₁) $ eq_empty_of_forall_not_mem $
+  from d.has_compl $ d.has_union h₂ (d.has_compl h₁) $ eq_empty_iff_forall_not_mem.2 $
     assume x ⟨h₁, h₂⟩, h₂ $ h h₁,
 have s₁ - s₂ = - (s₂ ∪ -s₁),
   by rw [compl_union, compl_compl, inter_comm]; refl,

analysis/metric_space.lean

@@ -164,7 +164,7 @@ def open_ball (x : α) (ε : ℝ) : set α := {y | dist y x < ε}
 def closed_ball (x : α) (ε : ℝ) := {y | dist y x ≤ ε}
 
 theorem open_ball_eq_empty_of_nonpos (hε : ε ≤ 0) : open_ball x ε = ∅ :=
-eq_empty_of_forall_not_mem $ assume y hy,
+eq_empty_iff_forall_not_mem.2 $ assume y hy,
   have dist y x < 0, from lt_of_lt_of_le hy hε,
   lt_irrefl 0 (lt_of_le_of_lt dist_nonneg this)
 

analysis/topology/topological_space.lean

@@ -771,7 +771,7 @@ instance inhabited_topological_space {α : Type u} : inhabited (topological_spac
 
 lemma t2_space_top : @t2_space α ⊤ :=
 { t2 := assume x y hxy, ⟨{x}, {y}, trivial, trivial, mem_insert _ _, mem_insert _ _,
-  eq_empty_of_forall_not_mem $ by intros z hz; simp at hz; cc⟩ }
+  eq_empty_iff_forall_not_mem.2 $ by intros z hz; simp at hz; cc⟩ }
 
 lemma le_of_nhds_le_nhds {t₁ t₂ : topological_space α} (h : ∀x, @nhds α t₂ x ≤ @nhds α t₁ x) :
   t₁ ≤ t₂ :=

analysis/topology/topological_structures.lean

@@ -198,7 +198,7 @@ instance ordered_topology.to_t2_space : t2_space α :=
   assume a b h,
   let ⟨u, v, hu, hv, ha, hb, h⟩ := is_open_prod_iff.mp this a b h in
   ⟨u, v, hu, hv, ha, hb,
-    set.eq_empty_of_forall_not_mem $ assume a ⟨h₁, h₂⟩,
+    set.eq_empty_iff_forall_not_mem.2 $ assume a ⟨h₁, h₂⟩,
     have a ≠ a, from @h (a, a) ⟨h₁, h₂⟩,
     this rfl⟩ }
 

data/bool.lean

@@ -16,6 +16,9 @@ show _ = to_bool true, by congr
 @[simp] theorem to_bool_false {h} : @to_bool false h = ff :=
 show _ = to_bool false, by congr
 
+@[simp] theorem to_bool_coe (b:bool) {h} : @to_bool b h = b :=
+(show _ = to_bool b, by congr).trans (by cases b; refl)
+
 @[simp] theorem coe_to_bool (p : Prop) [decidable p] : to_bool p ↔ p := to_bool_iff _
 
 theorem dichotomy (b : bool) : b = ff ∨ b = tt :=