bddBelow_range_of_small — Mathlib

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

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