closure_mono — Mathlib

English

If h ⊆ k are subsets of G, then closure(h) ≤ closure(k).

Русский

Если h ⊆ k — подмножества G, то closure(h) ≤ closure(k).

LaTeX

$$$ h \subseteq k \Rightarrow \mathrm{closure}(h) \le \mathrm{closure}(k) $$$

Lean4

/-- Subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
then `closure h ≤ closure k`. -/
@[to_additive (attr := gcongr) /-- Additive subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
          then `closure h ≤ closure k` -/
    ]
theorem closure_mono ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k :=
  (Subgroup.gi G).gc.monotone_l h'

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