upperClosure_pi — Mathlib

English

If s is clopen (closed and open) and bounded below, then its upperClosure is clopen.

Русский

Если s одновременно замкнуто и открыто и ограничено снизу, то upperClosure(s) также замкнуто и открыто.

LaTeX

$$$\forall s,\ IsClopen(s) \land BddBelow(s) \Rightarrow IsClopen(upperClosure(s)).$$$

Lean4

protected theorem upperClosure_pi (hs : IsClopen s) (hs' : BddBelow s) : IsClopen (upperClosure s : Set (ι → ℝ)) :=
  ⟨hs.1.upperClosure_pi hs', hs.2.upperClosure⟩

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