closure_le — Mathlib

English

The closure operator is monotone: closure(k) ≤ K iff k ⊆ K.

Русский

Замыкание монотонно: closure(k) ≤ K тогда, когда k ⊆ K.

LaTeX

$$closure(k) \le K \iff k \subseteq K$$

Lean4

/-- A subgroup `K` includes `closure k` if and only if it includes `k`. -/
@[to_additive (attr := simp) /-- An additive subgroup `K` includes `closure k` if and only if it includes `k` -/
    ]
theorem closure_le : closure k ≤ K ↔ k ⊆ K :=
  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩

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