mulSingle_mem_pi — Mathlib

English

For a fixed index i and element x ∈ M_i, the element Pi.mulSingle i x belongs to pi I S if and only if i ∈ I implies x ∈ S_i.

Русский

Для фиксированного индекса i и элемента x ∈ M_i, элемент Pi.mulSingle i x принадлежит π I S тогда и только тогда, когда i ∈ I подразумевает x ∈ S_i.

LaTeX

$$$ Pi.mulSingle i x ∈ pi I S \iff i ∈ I \rightarrow x ∈ S i $$$

Lean4

@[to_additive (attr := simp)]
theorem mulSingle_mem_pi [DecidableEq ι] {I : Set ι} {S : ∀ i, Submonoid (M i)} (i : ι) (x : M i) :
    Pi.mulSingle i x ∈ pi I S ↔ i ∈ I → x ∈ S i :=
  Set.update_mem_pi_iff_of_mem (one_mem (pi I _))

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