bddAbove_range_of_small — Mathlib

English

A small family of pre-games is bounded above: for a small index set ι and f : ι → PGame, there exists M with f(i) ≤ M for all i.

Русский

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

LaTeX

$$$\exists M : PGame, \forall i, f(i) \le M$$$

Lean4

/-- A small family of pre-games is bounded above. -/
theorem bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → PGame.{u}) : BddAbove (Set.range f) :=
  by
  let x : PGame.{u} := ⟨Σ i, (f <| (equivShrink.{u} ι).symm i).LeftMoves, PEmpty, fun x ↦ moveLeft _ x.2, PEmpty.elim⟩
  refine ⟨x, Set.forall_mem_range.2 fun i ↦ ?_⟩
  rw [← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]
  simpa [x] using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩

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