English
Let ι be finite and s ⊆ ℝ^ι. If s is closed and bounded above, then its lower closure is closed.
Русский
Пусть ι конечен и s ⊆ ℝ^ι. Если s замкнуто и ограничено сверху, то нижняя замыкание lowerClosure(s) замкнуто.
LaTeX
$$$\forall \iota \,[Finite\,\iota],\ \forall s\subseteq (\iota \to \mathbb{R}),\ IsClosed(s) \land BddAbove(s) \Rightarrow IsClosed(lowerClosure(s)).$$$
Lean4
protected theorem lowerClosure_pi (hs : IsClosed s) (hs' : BddAbove s) : IsClosed (lowerClosure s : Set (ι → ℝ)) :=
by
cases nonempty_fintype ι
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
choose g hg hfg using hf
haveI : BoundedGENhdsClass ℝ := by infer_instance
obtain ⟨a, ha⟩ := hx.bddBelow_range
obtain ⟨b, hb, φ, hφ, hbf⟩ :=
tendsto_subseq_of_bounded (hs'.isBounded_inter bddBelow_Ici) fun n ↦ ⟨hg n, (ha <| mem_range_self _).trans <| hfg _⟩
exact
⟨b, closure_minimal inter_subset_left hs hb, le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_atTop) hbf fun _ ↦ hfg _⟩
