add_closure_iUnion_range_single — Mathlib

English

The closure of the union over i of the ranges of single i is the top submonoid.

Русский

Замыкание объединения по i диапазонов одиночек порождает верхний подмонот.

LaTeX

$$$\\mathrm{AddSubmonoid}.closure\\big(\\bigcup_{i:\\lvert ι}\\mathrm{Set.range}(\\mathrm{single}\\, i)\\big) = \\top$$$

Lean4

@[simp]
theorem add_closure_iUnion_range_single : AddSubmonoid.closure (⋃ i : ι, Set.range (single i : β i → Π₀ i, β i)) = ⊤ :=
  top_unique fun x _ => by
    apply DFinsupp.induction x
    · exact AddSubmonoid.zero_mem _
    exact fun a b f _ _ hf =>
      AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

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