addSubmonoidClosure_one — Mathlib

English

In the natural numbers, the closure of {1} under addition generates all of N; i.e., the additive submonoid generated by 1 is the entire set.

Русский

В натуральных числах замыкание над множестом {1} по сложению даёт все натуральные числа.

LaTeX

$$$ closure(\{1\}) = ⊤ $ in AddSubmonoid on ℕ$$

Lean4

@[simp]
theorem addSubmonoidClosure_one : closure ({ 1 } : Set ℕ) = ⊤ :=
  by
  refine (eq_top_iff' _).2 <| Nat.rec (zero_mem _) ?_
  simp_rw [Nat.succ_eq_add_one]
  exact fun n hn ↦ AddSubmonoid.add_mem _ hn <| subset_closure <| Set.mem_singleton _

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