closure_insert_natCast — Mathlib

English

The closure of insert(n cast) s equals the closure of s for natural cast as well.

Русский

Замыкание вставки natCast равняется замыканию исходного множества для натурального приведения тоже.

LaTeX

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

Lean4

@[simp]
theorem closure_insert_natCast (n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s :=
  mod_cast closure_insert_intCast n s

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