lowerClosure_subset_closure — Mathlib

English

In IsScott α univ, the image of lowerClosure s is contained in the closure of s.

Русский

В IsScott α univ образ lowerClosure(s) содержится в closure(s).

LaTeX

$$$↑(\\mathrm{lowerClosure}(s)) \\subseteq \\overline{s}$$$

Lean4

theorem lowerClosure_subset_closure [IsScott α univ] : ↑(lowerClosure s) ⊆ closure s :=
  by
  convert closure.mono (@upperSet_le_scott α _)
  · rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]
    infer_instance
  · exact topology_eq α univ

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