exists_mem_closure_of_ge — Mathlib

English

There exists N such that for all m ≥ N, if setGcd(s) divides m, then m lies in the closure of s.

Русский

Существует N, что для всех m ≥ N, если setGcd(s) делит m, то m принадлежитclosure(s).

LaTeX

$$$\\exists n, \\forall m \\ge n,\\; \\mathrm{setGcd}(s) \\mid m \\Rightarrow m \\in \\mathrm{AddSubmonoid.closure}(s)$$$

Lean4

theorem exists_mem_closure_of_ge : ∃ n, ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s :=
  have ⟨_t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
  ⟨n, fun m ge dvd ↦ (Submodule.span_nat_eq_addSubmonoidClosure s).le (Submodule.span_mono hts (hn m ge dvd))⟩

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