mulSingle_mem_pi — Mathlib

English

For a fixed index i and element x in f i, Pi.mulSingle i x lies in pi I H iff i ∈ I implies x ∈ H i.

Русский

Для фиксированного индекса i и элемента x в f i, Pi.mulSingle i x принадлежит pi I H тогда, когда i ∈ I влечет x ∈ H i.

LaTeX

$$$ \Pi.\mathrm{mulSingle} i x \in \pi I H \iff i \in I \to x \in H i $$$

Lean4

@[to_additive (attr := simp)]
theorem mulSingle_mem_pi [DecidableEq η] {I : Set η} {H : ∀ i, Subgroup (f i)} (i : η) (x : f i) :
    Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i :=
  Set.update_mem_pi_iff_of_mem (one_mem (pi I H))

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