English
A small family of games has a lower bound; there exists x ∈ Game with x ≤ f(i) for all i.
Русский
Малое семейство игр имеет нижнюю границу: существует x ∈ Game, такой что x ≤ f(i) для каждого i.
LaTeX
$$$ \exists x\in \mathrm{Game}\;\forall i, x \le f(i) $$$
Lean4
/-- A small family of games is bounded below. -/
theorem 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