topologicalClosure_mono — Mathlib

English

The operator taking a star-subalgebra to its topological closure is monotone with respect to inclusion.

Русский

Оператор замыкания по включению монотонен: если s ≤ t, то s.topologicalClosure ≤ t.topologicalClosure.

LaTeX

$$If $s \le t$, then $s.topologicalClosure \le t.topologicalClosure$.$$

Lean4

theorem topologicalClosure_mono : Monotone (topologicalClosure : _ → StarSubalgebra R A) := fun _ S₂ h =>
  topologicalClosure_minimal (h.trans <| le_topologicalClosure S₂) (isClosed_topologicalClosure S₂)

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