English
Let ι be finite and s a subset of ℝ^ι. If s is closed and bounded below (in the product order), then its upper closure is a closed set in ℝ^ι.
Русский
Пусть ι конечен и s ⊆ ℝ^ι. Если s замкнуто и снизу ограничено по произведению порядка, то верхняя окрестность upperClosure(s) замкнута в ℝ^ι.
LaTeX
$$$\forall \iota \,[Finite\,\iota],\ \forall s\subseteq (\iota \to \mathbb{R}),\ IsClosed(s) \land BddBelow(s) \Rightarrow IsClosed(upperClosure(s)).$$$
Lean4
protected theorem upperClosure_pi (hs : IsClosed s) (hs' : BddBelow s) : IsClosed (upperClosure s : Set (ι → ℝ)) :=
by
cases nonempty_fintype ι
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
choose g hg hgf using hf
obtain ⟨a, ha⟩ := hx.bddAbove_range
obtain ⟨b, hb, φ, hφ, hbf⟩ :=
tendsto_subseq_of_bounded (hs'.isBounded_inter bddAbove_Iic) fun n ↦ ⟨hg n, (hgf _).trans <| ha <| mem_range_self _⟩
exact
⟨b, closure_minimal inter_subset_left hs hb, le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_atTop) fun _ ↦ hgf _⟩
