mem_closure_finset' — Mathlib

English

A variant of closure membership for a Finset s: x ∈ closure(s) iff there exists a : s → ℕ with x = ∏ i ∈ s, i.1^{a i}.

Русский

Вариант членства в замыкании для конечного множества s: x ∈ closure(s) тогда существует a : s → ℕ с x = ∏_{i ∈ s} i.1^{a i}.

LaTeX

$$$\text{For } s : \mathrm{Finset} M,\ x \in closure(s) \iff \exists a : s \to \mathbb{N},\ x = \prod_{i : s} i.1^{a i}$$$

Lean4

/-- A variant of `Submonoid.mem_closure_finset` using `s` as the index type. -/
@[to_additive /-- A variant of `AddSubmonoid.mem_closure_finset` using `s` as the index type. -/
    ]
theorem mem_closure_finset' {s : Finset M} : x ∈ closure s ↔ ∃ a : s → ℕ, x = ∏ i : s, i.1 ^ a i :=
  mem_closure_iff_of_fintype

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