bddBelow_of_small — Mathlib

English

For a small set s ⊆ PGame, there exists m with m ≤ x for all x ∈ s.

Русский

Для малого множества s ⊆ PGame существует m, такой что m ≤ x для всех x ∈ s.

LaTeX

$$$\exists m : PGame, \forall x \in s, m \le x$$$

Lean4

/-- A small set of pre-games is bounded below. -/
theorem bddBelow_of_small (s : Set PGame.{u}) [Small.{u} s] : BddBelow s := by
  simpa using bddBelow_range_of_small (Subtype.val : s → PGame.{u})

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