English
IsLUB of a set of functions equals pointwise IsLUBs of the evaluations.
Русский
Наибольший верхний предел множества функций эквивалентен по точкам наибольшим верхним пределам на соответствующих проекциях.
LaTeX
$$$ \\IsLUB s f \\iff \\forall a, \\IsLUB (\\mathrm{Function.eval}\\ a '' s) (f a) $$$
Lean4
theorem isLUB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : IsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a) := by
classical
refine ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H => ⟨?_, ?_⟩⟩
· suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
· exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
· exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
