bddAbove_range_of_small — Mathlib

English

A small family of games is bounded above: for any f : ι → Game with ι small, there exists x ∈ Game such that f(i) ≤ x for all i.

Русский

Маленькая семья игр ограничена сверху: существует некая G такая, что для всех i: f(i) ≤ G.

LaTeX

$$$ \exists x\in \mathrm{Game}\;\forall i, f(i) \le x $$$

Lean4

/-- A small family of games is bounded above. -/
theorem 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

Похожие утверждения