closure_mono — Mathlib

English

If s ⊆ t, then closure(s) ≤ closure(t).

Русский

Если s ⊆ t, то closure(s) ≤ closure(t).

LaTeX

$$$ s \\subseteq t \\Rightarrow \\mathrm{closure}(s) \\le \\mathrm{closure}(t) $$$

Lean4

/-- subsemigroup closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`. -/
@[to_additive (attr := gcongr) /-- Additive subsemigroup closure of a set is monotone in its
    argument: if `s ⊆ t`, then `closure s ≤ closure t` -/
    ]
theorem closure_mono ⦃s t : Set M⦄ (h : s ⊆ t) : closure s ≤ closure t :=
  closure_le.2 <| Subset.trans h subset_closure

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