one_mem_closure_iff — Mathlib

English

For any set s ⊆ ℕ, 1 belongs to AddSubmonoid.closure(s) if and only if 1 ∈ s.

Русский

Для любого множества s ⊆ ℕ верно: 1 принадлежит замыканию AddSubmonoid(s) тогда и только тогда, когда 1 ∈ s.

LaTeX

$$$1 \in \mathrm{AddSubmonoid.closure}(s) \iff 1 \in s$$$

Lean4

theorem one_mem_closure_iff {s : Set ℕ} : 1 ∈ AddSubmonoid.closure s ↔ 1 ∈ s :=
  by
  rw [← Submodule.span_nat_eq_addSubmonoidClosure]
  exact one_mem_span_iff

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