isGLB_pi — Mathlib

English

IsGLB of a set of functions equals pointwise IsGLBs of evaluations (dual of isLUB_pi).

Русский

Нижняя граница множества функций эквивалентна по точкам нижним границам значений функций.

LaTeX

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

Lean4

theorem isGLB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : IsGLB s f ↔ ∀ a, IsGLB (Function.eval a '' s) (f a) :=
  @isLUB_pi α (fun a => (π a)ᵒᵈ) _ s f

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