closure_insert_natCast — Mathlib

English

Inserting a natCast element into a set does not change its closure: closure(insert(n, s)) = closure(s).

Русский

Добавление элемента natCast к множеству не изменяет его замыкание: closure(insert(n, s)) = closure(s).

LaTeX

$$$\mathrm{closure}(\mathrm{insert}(n, s)) = \mathrm{closure}(s)$$$

Lean4

@[simp]
theorem closure_insert_natCast (n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s :=
  by
  rw [Set.insert_eq, closure_union]
  simp

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