bddBelow_range_of_small — Mathlib

English

A small family of pre-games is bounded below: there exists m with m ≤ f(i) for all i.

Русский

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

LaTeX

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

Lean4

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

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