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