mem_closure_iff_of_fintype — Mathlib

English

For a finite index set s ⊆ M, x ∈ closure s iff there exists a : s → ℕ with x = ∏ i in s, i.1^{a i}.

Русский

Для конечного множества индексов s ⊆ M, x ∈ closure s тогда существует a: s → ℕ с x = ∏ i∈s i.1^{a i}.

LaTeX

$$$\text{If } [\text{Fintype } s],\ x ∈ closure(s) \iff \exists a : s \to \mathbb{N},\ x = \prod_{i : s} i.1^{a i}$$$

Lean4

@[to_additive]
theorem mem_closure_iff_of_fintype {s : Set M} [Fintype s] : x ∈ closure s ↔ ∃ a : s → ℕ, x = ∏ i : s, i.1 ^ a i :=
  by
  conv_lhs => rw [← Subtype.range_coe (s := s)]
  exact mem_closure_range_iff_of_fintype

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