bddAbove_pi — Mathlib

English

A set s of functions is bounded above iff for every a, the image under evaluation at a is bounded above.

Русский

Множество функций ограничено сверху тогда, когда каждая фиксация аргумента даёт множество значений, ограниченное сверху.

LaTeX

$$$ \\IsBoundedAbove s \\iff \\forall a, \\IsBoundedAbove (\\mathrm{Function.eval}\\ a '' s) $$$

Lean4

theorem bddAbove_pi {s : Set (∀ a, π a)} : BddAbove s ↔ ∀ a, BddAbove (Function.eval a '' s) :=
  ⟨fun ⟨f, hf⟩ a ↦ ⟨f a, forall_mem_image.2 fun _ hg ↦ hf hg a⟩, fun h ↦
    ⟨fun a ↦ (h a).some, fun _ hg a ↦ (h a).some_mem <| mem_image_of_mem _ hg⟩⟩

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