bddBelow_pi — Mathlib

English

Dual of bddAbove_pi: BddBelow s iff ∀ a, BddBelow (Function.eval a '' s).

Русский

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

LaTeX

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

Lean4

theorem bddBelow_pi {s : Set (∀ a, π a)} : BddBelow s ↔ ∀ a, BddBelow (Function.eval a '' s) :=
  bddAbove_pi (π := fun a ↦ (π a)ᵒᵈ)

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