English
A small family of surreals is bounded above.
Русский
Малое семейство сурреалов ограничено сверху.
LaTeX
$$∀ ι [Small ι], f : ι → Surreal, BddAbove(Set.range f)$$
Lean4
/-- A small family of surreals is bounded above. -/
theorem 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⟩
