lowerClosure_pi — Mathlib

English

If s is clopen and bounded above, then the lowerClosure of s is clopen.

Русский

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

LaTeX

$$$\forall s,\ IsClopen(s) \land BddAbove(s) \Rightarrow IsClopen(lowerClosure(s)).$$$

Lean4

protected theorem lowerClosure_pi (hs : IsClopen s) (hs' : BddAbove s) : IsClopen (lowerClosure s : Set (ι → ℝ)) :=
  ⟨hs.1.lowerClosure_pi hs', hs.2.lowerClosure⟩

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