topologicalClosure_minimal — Mathlib

English

If S ⊆ T and T is closed, then the closure of S is contained in T; equivalently, the closure operation is monotone with respect to inclusion under a closed bound.

Русский

Если S ⊆ T и T замкнуто, то замыкание S содержится в T; замыкание монотонно по включению с учетом замкнутости.

LaTeX

$$$S \le T \Rightarrow S.topologicalClosure \le T.topologicalClosure$ (and with IsClosed(T): $S.topologicalClosure \le T)$$$

Lean4

theorem topologicalClosure_minimal (s : Submodule R M) {t : Submodule R M} (h : s ≤ t) (ht : IsClosed (t : Set M)) :
    s.topologicalClosure ≤ t :=
  closure_minimal h ht

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