subset_closure — Mathlib

English

The set k is contained in its closure: k ⊆ closure(k).

Русский

Множество k содержится в своем замыкании: k ⊆ closure(k).

LaTeX

$$k \subseteq closure(k)$$

Lean4

/-- The subgroup generated by a set includes the set. -/
@[to_additive (attr := simp, aesop safe 20 (rule_sets := [SetLike])) /--
    The `AddSubgroup` generated by a set includes the set. -/
    ]
theorem subset_closure : k ⊆ closure k := fun _ hx => mem_closure.2 fun _ hK => hK hx

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