From edd0f932d56b592fb1e13c27418f5d7b3e69baa8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 20 Jul 2022 16:22:53 +0000 Subject: [PATCH] feat(set_theory/ordinal/basic): dot notation lemmas + golf (#15348) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We introduce dot notation lemmas for proving something of the form `type r < type s` or `type r ≤ type s` by providing a principal segment, an initial segment, or a relation embedding. We rename `type_le` and `type_le'` to `type_le_iff` and `type_le_iff'` for consistency with `type_lt_iff` (which can't be renamed to `type_lt`, as this is an existing theorem about `type (<)`). We could introduce `lift` variants of these, but I'd rather wait until #15041 is merged, at which point I can do the analogous refactor on ordinals. --- src/set_theory/cardinal/cofinality.lean | 6 +++--- src/set_theory/ordinal/arithmetic.lean | 15 +++++---------- src/set_theory/ordinal/basic.lean | 24 ++++++++++++++++-------- 3 files changed, 24 insertions(+), 21 deletions(-) diff --git a/src/set_theory/cardinal/cofinality.lean b/src/set_theory/cardinal/cofinality.lean index e55bbd14263d5..a2c96d6953220 100644 --- a/src/set_theory/cardinal/cofinality.lean +++ b/src/set_theory/cardinal/cofinality.lean @@ -162,8 +162,8 @@ begin { refine ⟨T, this, le_antisymm _ (cardinal.ord_le.2 $ cof_type_le this)⟩, rw [← e, e'], - refine type_le'.2 ⟨rel_embedding.of_monotone - (λ a, ⟨a, let ⟨aS, _⟩ := a.2 in aS⟩) (λ a b h, _)⟩, + refine (rel_embedding.of_monotone (λ a : T, (⟨a, let ⟨aS, _⟩ := a.2 in aS⟩ : S)) (λ a b h, _)) + .ordinal_type_le, rcases a with ⟨a, aS, ha⟩, rcases b with ⟨b, bS, hb⟩, change s ⟨a, _⟩ ⟨b, _⟩, refine ((trichotomous_of s _ _).resolve_left (λ hn, _)).resolve_left _, @@ -507,7 +507,7 @@ begin let r' := subrel r {i | ∀ j, r j i → f j < f i}, let hrr' : r' ↪r r := subrel.rel_embedding _ _, haveI := hrr'.is_well_order, - refine ⟨_, _, (type_le'.2 ⟨hrr'⟩).trans _, λ i j _ h _, (enum r' j h).prop _ _, + refine ⟨_, _, hrr'.ordinal_type_le.trans _, λ i j _ h _, (enum r' j h).prop _ _, le_antisymm (blsub_le (λ i hi, lsub_le_iff.1 hf.le _)) _⟩, { rw [←hι, hr] }, { change r (hrr'.1 _ ) (hrr'.1 _ ), diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index d797e3f36a753..f99e15ce4a64b 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -480,7 +480,7 @@ induction_on a (λ α r _, induction_on b $ λ β s _ h H l, begin rw [←typein_lt_typein (sum.lex r s), typein_enum], have := H _ (h.2 _ (typein_lt_type s x)), rw [add_succ, succ_le_iff] at this, - refine (type_le'.2 ⟨rel_embedding.of_monotone (λ a, _) (λ a b, _)⟩).trans_lt this, + refine (rel_embedding.of_monotone (λ a, _) (λ a b, _)).ordinal_type_le.trans_lt this, { rcases a with ⟨a | b, h⟩, { exact sum.inl a }, { exact sum.inr ⟨b, by cases h; assumption⟩ } }, @@ -640,9 +640,8 @@ theorem mul_succ (a b : ordinal) : a * succ b = a * b + a := mul_add_one a b instance mul_covariant_class_le : covariant_class ordinal.{u} ordinal.{u} (*) (≤) := ⟨λ c a b, quotient.induction_on₃ a b c $ λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩, begin resetI, - refine type_le'.2 ⟨rel_embedding.of_monotone - (λ a, (f a.1, a.2)) - (λ a b h, _)⟩, clear_, + refine (rel_embedding.of_monotone (λ a : α × γ, (f a.1, a.2)) (λ a b h, _)).ordinal_type_le, + clear_, cases h with a₁ b₁ a₂ b₂ h' a b₁ b₂ h', { exact prod.lex.left _ _ (f.to_rel_embedding.map_rel_iff.2 h') }, { exact prod.lex.right _ h' } @@ -651,9 +650,7 @@ end⟩ instance mul_swap_covariant_class_le : covariant_class ordinal.{u} ordinal.{u} (swap (*)) (≤) := ⟨λ c a b, quotient.induction_on₃ a b c $ λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩, begin resetI, - refine type_le'.2 ⟨rel_embedding.of_monotone - (λ a, (a.1, f a.2)) - (λ a b h, _)⟩, + refine (rel_embedding.of_monotone (λ a : γ × α, (a.1, f a.2)) (λ a b h, _)).ordinal_type_le, cases h with a₁ b₁ a₂ b₂ h' a b₁ b₂ h', { exact prod.lex.left _ _ h' }, { exact prod.lex.right _ (f.to_rel_embedding.map_rel_iff.2 h') } @@ -676,9 +673,7 @@ begin have := H _ (h.2 _ (typein_lt_type s b)), rw mul_succ at this, have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this, - refine (type_le'.2 _).trans_lt this, - constructor, - refine rel_embedding.of_monotone (λ a, _) (λ a b, _), + refine (rel_embedding.of_monotone (λ a, _) (λ a b, _)).ordinal_type_le.trans_lt this, { rcases a with ⟨⟨b', a'⟩, h⟩, by_cases e : b = b', { refine sum.inr ⟨a', _⟩, diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean index f9a434656254a..c5030e43062cc 100644 --- a/src/set_theory/ordinal/basic.lean +++ b/src/set_theory/ordinal/basic.lean @@ -197,18 +197,27 @@ add_decl_doc ordinal.partial_order.le a function embedding `r` as a principal segment of `s`. -/ add_decl_doc ordinal.partial_order.lt -theorem type_le {α β} {r : α → α → Prop} {s : β → β → Prop} +theorem type_le_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] : type r ≤ type s ↔ nonempty (r ≼i s) := iff.rfl -theorem type_le' {α β} {r : α → α → Prop} {s : β → β → Prop} +theorem type_le_iff' {α β} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] : type r ≤ type s ↔ nonempty (r ↪r s) := ⟨λ ⟨f⟩, ⟨f⟩, λ ⟨f⟩, ⟨f.collapse⟩⟩ +theorem _root_.initial_seg.ordinal_type_le {α β} {r : α → α → Prop} {s : β → β → Prop} + [is_well_order α r] [is_well_order β s] (h : r ≼i s) : type r ≤ type s := ⟨h⟩ + +theorem _root_.rel_embedding.ordinal_type_le {α β} {r : α → α → Prop} {s : β → β → Prop} + [is_well_order α r] [is_well_order β s] (h : r ↪r s) : type r ≤ type s := ⟨h.collapse⟩ + @[simp] theorem type_lt_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] : type r < type s ↔ nonempty (r ≺i s) := iff.rfl +theorem _root_.principal_seg.ordinal_type_lt {α β} {r : α → α → Prop} {s : β → β → Prop} + [is_well_order α r] [is_well_order β s] (h : r ≺i s) : type r < type s := ⟨h⟩ + /-- Given two ordinals `α ≤ β`, then `initial_seg_out α β` is the initial segment embedding of `α` to `β`, as map from a model type for `α` to a model type for `β`. -/ def initial_seg_out {α β : ordinal} (h : α ≤ β) : @@ -637,14 +646,13 @@ instance add_swap_covariant_class_le : covariant_class ordinal.{u} ordinal.{u} ( ⟨λ c a b h, begin revert h c, exact ( induction_on a $ λ α₁ r₁ hr₁, induction_on b $ λ α₂ r₂ hr₂ ⟨⟨⟨f, fo⟩, fi⟩⟩ c, - induction_on c $ λ β s hs, (@type_le' _ _ _ _ - (@sum.lex.is_well_order _ _ _ _ hr₁ hs) - (@sum.lex.is_well_order _ _ _ _ hr₂ hs)).2 - ⟨⟨f.sum_map (embedding.refl _), λ a b, begin + induction_on c $ λ β s hs, by exactI + @rel_embedding.ordinal_type_le _ _ (sum.lex r₁ s) (sum.lex r₂ s) _ _ + ⟨f.sum_map (embedding.refl _), λ a b, begin split; intro H, { cases a with a a; cases b with b b; cases H; constructor; [rwa ← fo, assumption] }, { cases H; constructor; [rwa fo, assumption] } - end⟩⟩) + end⟩) end⟩ theorem le_add_right (a b : ordinal) : a ≤ a + b := @@ -899,7 +907,7 @@ let ⟨r, _, e⟩ := ord_eq α in begin { cases h with f, have g := rel_embedding.preimage f s, haveI := rel_embedding.is_well_order g, - exact le_trans (ord_le_type _) (type_le'.2 ⟨g⟩) } + exact le_trans (ord_le_type _) g.ordinal_type_le } end theorem gc_ord_card : galois_connection ord card := λ _ _, ord_le