From 0e9d0030b7ff88fbc31b107a95a2f99d54709aca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 9 Mar 2024 22:29:28 +0000 Subject: [PATCH] feat: Small sets of games/surreals are bounded (#10458) Finish forwarding porting https://github.com/leanprover-community/mathlib/pull/15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov Co-authored-by: timotree3 --- Mathlib/SetTheory/Game/Basic.lean | 26 +++++++++++++- Mathlib/SetTheory/Surreal/Basic.lean | 52 +++++++++++++++++++++++++++- 2 files changed, 76 insertions(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean index ce28787a09218..0340a48017df7 100644 --- a/Mathlib/SetTheory/Game/Basic.lean +++ b/Mathlib/SetTheory/Game/Basic.lean @@ -7,7 +7,7 @@ import Mathlib.Data.Int.Basic import Mathlib.SetTheory.Game.PGame import Mathlib.Tactic.Abel -#align_import set_theory.game.basic from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1" +#align_import set_theory.game.basic from "leanprover-community/mathlib"@"8900d545017cd21961daa2a1734bb658ef52c618" /-! # Combinatorial games. @@ -202,6 +202,30 @@ instance orderedAddCommGroup : OrderedAddCommGroup Game := add_le_add_left := @add_le_add_left _ _ _ Game.covariantClass_add_le } #align game.ordered_add_comm_group SetTheory.Game.orderedAddCommGroup +/-- A small family of games is bounded above. -/ +lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) : + BddAbove (Set.range f) := by + obtain ⟨x, hx⟩ := PGame.bddAbove_range_of_small (Quotient.out ∘ f) + refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩ + simpa [PGame.le_iff_game_le] using hx $ Set.mem_range_self i + +/-- A small set of games is bounded above. -/ +lemma bddAbove_of_small (s : Set Game.{u}) [Small.{u} s] : BddAbove s := by + simpa using bddAbove_range_of_small (Subtype.val : s → Game.{u}) +#align game.bdd_above_of_small SetTheory.Game.bddAbove_of_small + +/-- A small family of games is bounded below. -/ +lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) : + BddBelow (Set.range f) := by + obtain ⟨x, hx⟩ := PGame.bddBelow_range_of_small (Quotient.out ∘ f) + refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩ + simpa [PGame.le_iff_game_le] using hx $ Set.mem_range_self i + +/-- A small set of games is bounded below. -/ +lemma bddBelow_of_small (s : Set Game.{u}) [Small.{u} s] : BddBelow s := by + simpa using bddBelow_range_of_small (Subtype.val : s → Game.{u}) +#align game.bdd_below_of_small SetTheory.Game.bddBelow_of_small + end Game namespace PGame diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean index a9c0dbc244989..981c9ca678102 100644 --- a/Mathlib/SetTheory/Surreal/Basic.lean +++ b/Mathlib/SetTheory/Surreal/Basic.lean @@ -6,7 +6,7 @@ Authors: Mario Carneiro, Scott Morrison import Mathlib.Algebra.Order.Hom.Monoid import Mathlib.SetTheory.Game.Ordinal -#align_import set_theory.surreal.basic from "leanprover-community/mathlib"@"ee02a30e209a2a77b93eac1254e8c66e76192f54" +#align_import set_theory.surreal.basic from "leanprover-community/mathlib"@"8900d545017cd21961daa2a1734bb658ef52c618" /-! # Surreal numbers @@ -322,6 +322,9 @@ instance instLE : LE Surreal := ⟨lift₂ (fun x y _ _ => x ≤ y) fun _ _ _ _ hx hy => propext (le_congr hx hy)⟩ #align surreal.has_le Surreal.instLE +@[simp] +lemma mk_le_mk {x y : PGame.{u}} {hx hy} : mk x hx ≤ mk y hy ↔ x ≤ y := Iff.rfl + instance instLT : LT Surreal := ⟨lift₂ (fun x y _ _ => x < y) fun _ _ _ _ hx hy => propext (lt_congr hx hy)⟩ #align surreal.has_lt Surreal.instLT @@ -388,6 +391,53 @@ theorem nat_toGame : ∀ n : ℕ, toGame n = n := map_natCast' _ one_toGame #align surreal.nat_to_game Surreal.nat_toGame +#noalign upper_bound_numeric +#noalign lower_bound_numeric + +/-- A small family of surreals is bounded above. -/ +lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Surreal.{u}) : + BddAbove (Set.range f) := by + induction' f using Quotient.induction_on_pi with f + let g : ι → PGame.{u} := Subtype.val ∘ f + have hg (i) : (g i).Numeric := Subtype.prop _ + conv in (⟦f _⟧) => + change mk (g i) (hg i) + clear_value g + clear f + let x : PGame.{u} := ⟨Σ i, (g <| (equivShrink.{u} ι).symm i).LeftMoves, PEmpty, + fun x ↦ moveLeft _ x.2, PEmpty.elim⟩ + refine ⟨mk x (.mk (by simp [x]) (fun _ ↦ (hg _).moveLeft _) (by simp [x])), + Set.forall_mem_range.2 fun i ↦ ?_⟩ + rw [mk_le_mk, ← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf] + simpa [x] using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩ + +/-- A small set of surreals is bounded above. -/ +lemma bddAbove_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddAbove s := by + simpa using bddAbove_range_of_small (Subtype.val : s → Surreal.{u}) +#align surreal.bdd_above_of_small Surreal.bddAbove_of_small + +/-- A small family of surreals is bounded below. -/ +lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Surreal.{u}) : + BddBelow (Set.range f) := by + induction' f using Quotient.induction_on_pi with f + let g : ι → PGame.{u} := Subtype.val ∘ f + have hg (i) : (g i).Numeric := Subtype.prop _ + conv in (⟦f _⟧) => + change mk (g i) (hg i) + clear_value g + clear f + let x : PGame.{u} := ⟨PEmpty, Σ i, (g <| (equivShrink.{u} ι).symm i).RightMoves, + PEmpty.elim, fun x ↦ moveRight _ x.2⟩ + refine ⟨mk x (.mk (by simp [x]) (by simp [x]) (fun _ ↦ (hg _).moveRight _) ), + Set.forall_mem_range.2 fun i ↦ ?_⟩ + rw [mk_le_mk, ← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf] + simpa [x] using fun j ↦ @lf_moveRight x ⟨equivShrink ι i, j⟩ + +/-- A small set of surreals is bounded below. -/ +lemma bddBelow_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddBelow s := by + simpa using bddBelow_range_of_small (Subtype.val : s → Surreal.{u}) +#align surreal.bdd_below_of_small Surreal.bddBelow_of_small + end Surreal open Surreal