pi_mem_of_mulSingle_mem — Mathlib

English

If η is finite and for a given x ∈ ∏_i f_i, π_i(x_i) ∈ H for every i, then x ∈ H.

Русский

Если множество индексов η конечно и для данного x ∈ ∏_i f_i выполняется, что Pi.mulSingle i (x_i) ∈ H для каждого i, то x ∈ H.

LaTeX

$$$[\text{Finite }\eta] \Rightarrow (\forall i, \Pi.mulSingle i (x_i) \in H) \Rightarrow x \in H$$$

Lean4

@[to_additive]
theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : S} (x : Π i, f i) (h : ∀ i, Pi.mulSingle i (x i) ∈ H) :
    x ∈ H := by
  cases nonempty_fintype η
  exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

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