From f13e5dfdaf7f8267bdeefd8fb168aafdd3ef6950 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 28 May 2022 17:52:57 +0000 Subject: [PATCH] refactor(set_theory/*) rename `wf` lemmas to `lt_wf` (#14417) This is done for consistency with the rest of `mathlib` (`nat.lt_wf`, `enat.lt_wf`, `finset.lt_wf`, ...) --- src/set_theory/cardinal/basic.lean | 10 +++++----- src/set_theory/cardinal/ordinal.lean | 2 +- src/set_theory/ordinal/arithmetic.lean | 22 +++++++++++----------- src/set_theory/ordinal/basic.lean | 25 +++++++++++-------------- src/set_theory/ordinal/notation.lean | 7 +++---- 5 files changed, 31 insertions(+), 35 deletions(-) diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index a7ee64faa27cf..ee0f58c9dca64 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -512,7 +512,7 @@ theorem le_min {ι I} {f : ι → cardinal} {a} : a ≤ cardinal.min I f ↔ ∀ ⟨λ h i, le_trans h (min_le _ _), λ h, let ⟨i, e⟩ := min_eq I f in e.symm ▸ h i⟩ -protected theorem wf : @well_founded cardinal.{u} (<) := +protected theorem lt_wf : @well_founded cardinal.{u} (<) := ⟨λ a, classical.by_contradiction $ λ h, let ι := {c :cardinal // ¬ acc (<) c}, f : ι → cardinal := subtype.val, @@ -521,13 +521,13 @@ protected theorem wf : @well_founded cardinal.{u} (<) := classical.by_contradiction $ λ hj, h' $ by have := min_le f ⟨j, hj⟩; rwa hi at this))⟩ -instance has_wf : @has_well_founded cardinal.{u} := ⟨(<), cardinal.wf⟩ +instance has_wf : @has_well_founded cardinal.{u} := ⟨(<), cardinal.lt_wf⟩ instance : conditionally_complete_linear_order_bot cardinal := -cardinal.wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (cardinal.zero_le _) $ - not_lt.1 (cardinal.wf.not_lt_min set.univ ⟨0, mem_univ _⟩ (mem_univ 0)) +cardinal.lt_wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (cardinal.zero_le _) $ + not_lt.1 (cardinal.lt_wf.not_lt_min set.univ ⟨0, mem_univ _⟩ (mem_univ 0)) -instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.wf⟩ +instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.lt_wf⟩ /-- Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`. -/ instance : succ_order cardinal := diff --git a/src/set_theory/cardinal/ordinal.lean b/src/set_theory/cardinal/ordinal.lean index b7ac9c938aec3..f800402dae50f 100644 --- a/src/set_theory/cardinal/ordinal.lean +++ b/src/set_theory/cardinal/ordinal.lean @@ -305,7 +305,7 @@ begin (by simpa only [mul_one] using mul_le_mul_left' (one_lt_omega.le.trans h) c), -- the only nontrivial part is `c * c ≤ c`. We prove it inductively. - refine acc.rec_on (cardinal.wf.apply c) (λ c _, + refine acc.rec_on (cardinal.lt_wf.apply c) (λ c _, quotient.induction_on c $ λ α IH ol, _) h, -- consider the minimal well-order `r` on `α` (a type with cardinality `c`). rcases ord_eq α with ⟨r, wo, e⟩, resetI, diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 15e98d280e0e4..25bb54e799a02 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -319,7 +319,7 @@ or.inr $ or.inr ⟨o0, λ a, (succ_lt_of_not_succ h).2⟩ @[elab_as_eliminator] def limit_rec_on {C : ordinal → Sort*} (o : ordinal) (H₁ : C 0) (H₂ : ∀ o, C o → C (succ o)) (H₃ : ∀ o, is_limit o → (∀ o' < o, C o') → C o) : C o := -wf.fix (λ o IH, +lt_wf.fix (λ o IH, if o0 : o = 0 then by rw o0; exact H₁ else if h : ∃ a, o = succ a then by rw ← succ_pred_iff_is_succ.2 h; exact @@ -327,13 +327,13 @@ wf.fix (λ o IH, else H₃ _ ⟨o0, λ a, (succ_lt_of_not_succ h).2⟩ IH) o @[simp] theorem limit_rec_on_zero {C} (H₁ H₂ H₃) : @limit_rec_on C 0 H₁ H₂ H₃ = H₁ := -by rw [limit_rec_on, wf.fix_eq, dif_pos rfl]; refl +by rw [limit_rec_on, lt_wf.fix_eq, dif_pos rfl]; refl @[simp] theorem limit_rec_on_succ {C} (o H₁ H₂ H₃) : @limit_rec_on C (succ o) H₁ H₂ H₃ = H₂ o (@limit_rec_on C o H₁ H₂ H₃) := begin have h : ∃ a, succ o = succ a := ⟨_, rfl⟩, - rw [limit_rec_on, wf.fix_eq, dif_neg (succ_ne_zero o), dif_pos h], + rw [limit_rec_on, lt_wf.fix_eq, dif_neg (succ_ne_zero o), dif_pos h], generalize : limit_rec_on._proof_2 (succ o) h = h₂, generalize : limit_rec_on._proof_3 (succ o) h = h₃, revert h₂ h₃, generalize e : pred (succ o) = o', intros, @@ -342,7 +342,7 @@ end @[simp] theorem limit_rec_on_limit {C} (o H₁ H₂ H₃ h) : @limit_rec_on C o H₁ H₂ H₃ = H₃ o h (λ x h, @limit_rec_on C x H₁ H₂ H₃) := -by rw [limit_rec_on, wf.fix_eq, dif_neg h.1, dif_neg (not_succ_of_is_limit h)]; refl +by rw [limit_rec_on, lt_wf.fix_eq, dif_neg h.1, dif_neg (not_succ_of_is_limit h)]; refl instance order_top_out_succ (o : ordinal) : order_top (succ o).out.α := ⟨_, le_enum_succ⟩ @@ -414,7 +414,7 @@ theorem is_normal.inj {f} (H : is_normal f) {a b} : f a = f b ↔ a = b := by simp only [le_antisymm_iff, H.le_iff] theorem is_normal.self_le {f} (H : is_normal f) (a) : a ≤ f a := -wf.self_le_of_strict_mono H.strict_mono a +lt_wf.self_le_of_strict_mono H.strict_mono a theorem is_normal.le_set {f} (H : is_normal f) (p : set ordinal) (p0 : p.nonempty) (b) (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) {o : ordinal} : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o := @@ -1653,13 +1653,13 @@ variables {S : set ordinal.{u}} /-- Enumerator function for an unbounded set of ordinals. -/ def enum_ord (S : set ordinal.{u}) : ordinal → ordinal := -wf.fix (λ o f, Inf (S ∩ set.Ici (blsub.{u u} o f))) +lt_wf.fix (λ o f, Inf (S ∩ set.Ici (blsub.{u u} o f))) /-- The equation that characterizes `enum_ord` definitionally. This isn't the nicest expression to work with, so consider using `enum_ord_def` instead. -/ theorem enum_ord_def' (o) : enum_ord S o = Inf (S ∩ set.Ici (blsub.{u u} o (λ a _, enum_ord S a))) := -wf.fix_eq _ _ +lt_wf.fix_eq _ _ /-- The set in `enum_ord_def'` is nonempty. -/ theorem enum_ord_def'_nonempty (hS : unbounded (<) S) (a) : (S ∩ set.Ici a).nonempty := @@ -1696,7 +1696,7 @@ lemma enum_ord_def_nonempty (hS : unbounded (<) S) {o} : @[simp] theorem enum_ord_range {f : ordinal → ordinal} (hf : strict_mono f) : enum_ord (range f) = f := funext (λ o, begin - apply wf.induction o, + apply ordinal.induction o, intros a H, rw enum_ord_def a, have Hfa : f a ∈ range f ∩ {b | ∀ c, c < a → enum_ord (range f) c < b} := @@ -1724,7 +1724,7 @@ end theorem enum_ord_le_of_subset {S T : set ordinal} (hS : unbounded (<) S) (hST : S ⊆ T) (a) : enum_ord T a ≤ enum_ord S a := begin - apply wf.induction a, + apply ordinal.induction a, intros b H, rw enum_ord_def, exact cInf_le' ⟨hST (enum_ord_mem hS b), λ c h, (H c h).trans_lt (enum_ord_strict_mono hS h)⟩ @@ -1740,7 +1740,7 @@ theorem enum_ord_surjective (hS : unbounded (<) S) : ∀ s ∈ S, ∃ a, enum_or exact (enum_ord_strict_mono hS hab).trans_le hb }, { by_contra' h, exact (le_cSup ⟨s, λ a, - (wf.self_le_of_strict_mono (enum_ord_strict_mono hS) a).trans⟩ + (lt_wf.self_le_of_strict_mono (enum_ord_strict_mono hS) a).trans⟩ (enum_ord_succ_le hS hs h)).not_lt (lt_succ _) } end⟩ @@ -1758,7 +1758,7 @@ theorem eq_enum_ord (f : ordinal → ordinal) (hS : unbounded (<) S) : begin split, { rintro ⟨h₁, h₂⟩, - rwa [←wf.eq_strict_mono_iff_eq_range h₁ (enum_ord_strict_mono hS), range_enum_ord hS] }, + rwa [←lt_wf.eq_strict_mono_iff_eq_range h₁ (enum_ord_strict_mono hS), range_enum_ord hS] }, { rintro rfl, exact ⟨enum_ord_strict_mono hS, range_enum_ord hS⟩ } end diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean index 8135c398174e4..7bf1a8774983c 100644 --- a/src/set_theory/ordinal/basic.lean +++ b/src/set_theory/ordinal/basic.lean @@ -695,7 +695,7 @@ lemma rel_iso_enum {α β : Type u} {r : α → α → Prop} {s : β → β → enum s o (by {convert hr using 1, apply quotient.sound, exact ⟨f.symm⟩ }) := rel_iso_enum' _ _ _ _ -theorem wf : @well_founded ordinal (<) := +theorem lt_wf : @well_founded ordinal (<) := ⟨λ a, induction_on a $ λ α r wo, by exactI suffices ∀ a, acc (<) (typein r a), from ⟨_, λ o h, let ⟨a, e⟩ := typein_surj r h in e ▸ this a⟩, @@ -704,13 +704,13 @@ suffices ∀ a, acc (<) (typein r a), from exact IH _ ((typein_lt_typein r).1 h) end⟩⟩ -instance : has_well_founded ordinal := ⟨(<), wf⟩ +instance : has_well_founded ordinal := ⟨(<), lt_wf⟩ /-- Reformulation of well founded induction on ordinals as a lemma that works with the `induction` tactic, as in `induction i using ordinal.induction with i IH`. -/ lemma induction {p : ordinal.{u} → Prop} (i : ordinal.{u}) (h : ∀ j, (∀ k, k < j → p k) → p j) : p i := -ordinal.wf.induction i h +lt_wf.induction i h /-- Principal segment version of the `typein` function, embedding a well order into ordinals as a principal segment. -/ @@ -1022,6 +1022,8 @@ instance : linear_order ordinal := decidable_le := classical.dec_rel _, ..ordinal.partial_order } +instance : is_well_order ordinal (<) := ⟨lt_wf⟩ + private theorem succ_le_iff' {a b : ordinal} : a + 1 ≤ b ↔ a < b := ⟨lt_of_lt_of_le (induction_on a $ λ α r _, ⟨⟨⟨⟨λ x, sum.inl x, λ _ _, sum.inl.inj⟩, λ _ _, sum.lex_inl_inl⟩, @@ -1051,8 +1053,6 @@ instance : succ_order ordinal.{u} := succ_order.of_succ_le_iff (λ o, o + 1) (λ @[simp] theorem add_one_eq_succ (o : ordinal) : o + 1 = succ o := rfl -instance : is_well_order ordinal (<) := ⟨wf⟩ - @[simp] lemma typein_le_typein (r : α → α → Prop) [is_well_order α r] {x x' : α} : typein r x ≤ typein r x' ↔ ¬r x' x := by rw [←not_lt, typein_lt_typein] @@ -1163,13 +1163,13 @@ by simp only [lift.principal_seg_top, univ_id] /-- The minimal element of a nonempty family of ordinals -/ def min {ι} (I : nonempty ι) (f : ι → ordinal) : ordinal := -wf.min (set.range f) (let ⟨i⟩ := I in ⟨_, set.mem_range_self i⟩) +lt_wf.min (set.range f) (let ⟨i⟩ := I in ⟨_, set.mem_range_self i⟩) theorem min_eq {ι} (I) (f : ι → ordinal) : ∃ i, min I f = f i := -let ⟨i, e⟩ := wf.min_mem (set.range f) _ in ⟨i, e.symm⟩ +let ⟨i, e⟩ := lt_wf.min_mem (set.range f) _ in ⟨i, e.symm⟩ theorem min_le {ι I} (f : ι → ordinal) (i) : min I f ≤ f i := -le_of_not_gt $ wf.not_lt_min (set.range f) _ (set.mem_range_self i) +le_of_not_gt $ lt_wf.not_lt_min (set.range f) _ (set.mem_range_self i) theorem le_min {ι I} {f : ι → ordinal} {a} : a ≤ min I f ↔ ∀ i, a ≤ f i := ⟨λ h i, le_trans h (min_le _ _), @@ -1182,8 +1182,8 @@ by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $ by have := min_le (lift ∘ f) j; rwa e at this) instance : conditionally_complete_linear_order_bot ordinal := -wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (ordinal.zero_le _) $ - not_lt.1 (wf.not_lt_min set.univ ⟨0, mem_univ _⟩ (mem_univ 0)) +lt_wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (ordinal.zero_le _) $ + not_lt.1 (lt_wf.not_lt_min set.univ ⟨0, mem_univ _⟩ (mem_univ 0)) @[simp] lemma bot_eq_zero : (⊥ : ordinal) = 0 := rfl @@ -1198,10 +1198,7 @@ theorem eq_zero_or_pos : ∀ a : ordinal, a = 0 ∨ 0 < a := eq_bot_or_bot_lt @[simp] theorem Inf_empty : Inf (∅ : set ordinal) = 0 := -begin - change dite _ (wf.min ∅) (λ _, 0) = 0, - simp only [not_nonempty_empty, not_false_iff, dif_neg] -end +dif_neg not_nonempty_empty end ordinal diff --git a/src/set_theory/ordinal/notation.lean b/src/set_theory/ordinal/notation.lean index 1c8a21f3d260b..1f88fa38352a8 100644 --- a/src/set_theory/ordinal/notation.lean +++ b/src/set_theory/ordinal/notation.lean @@ -833,8 +833,8 @@ instance : preorder nonote := instance : has_zero nonote := ⟨⟨0, NF.zero⟩⟩ instance : inhabited nonote := ⟨0⟩ -theorem wf : @well_founded nonote (<) := inv_image.wf repr ordinal.wf -instance : has_well_founded nonote := ⟨(<), wf⟩ +theorem lt_wf : @well_founded nonote (<) := inv_image.wf repr ordinal.lt_wf +instance : has_well_founded nonote := ⟨(<), lt_wf⟩ /-- Convert a natural number to an ordinal notation -/ def of_nat (n : ℕ) : nonote := ⟨of_nat n, ⟨⟨_, NF_below_of_nat _⟩⟩⟩ @@ -852,8 +852,7 @@ theorem cmp_compares : ∀ a b : nonote, (cmp a b).compares a b end instance : linear_order nonote := linear_order_of_compares cmp cmp_compares - -instance : is_well_order nonote (<) := ⟨wf⟩ +instance : is_well_order nonote (<) := ⟨lt_wf⟩ /-- Asserts that `repr a < ω ^ repr b`. Used in `nonote.rec_on` -/ def below (a b : nonote) : Prop := NF_below a.1 (repr b)