threeGPFree_pi — Mathlib

English

If each s i is ThreeGPFree, then the product set over i is ThreeGPFree.

Русский

Если для каждого i множество s i является ThreeGPFree, то их произведение по индексу i также ThreeGPFree.

LaTeX

$$$$ \\forall i, \\text{ThreeGPFree}(s_i) \\Rightarrow \\text{ThreeGPFree}\\left(\\prod_{i} s_i\\right). $$$$

Lean4

@[to_additive]
theorem threeGPFree_pi {ι : Type*} {α : ι → Type*} [∀ i, Monoid (α i)] {s : ∀ i, Set (α i)}
    (hs : ∀ i, ThreeGPFree (s i)) : ThreeGPFree ((univ : Set ι).pi s) := fun _ ha _ hb _ hc h ↦
  funext fun i => hs i (ha i trivial) (hb i trivial) (hc i trivial) <| congr_fun h i

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