le_pi_iff — Mathlib

English

For I, S, J with J a submonoid of the product, J ≤ pi I S if and only if for all i ∈ I, J ≤ comap (Pi.evalMonoidHom M i) (S i).

Русский

Для I, S, J: J ≤ π I S тогда и только тогда, когда для каждого i ∈ I выполняется J ≤ comap (Pi.evalMonoidHom M i) (S i).

LaTeX

$$$ J \le \pi I S \iff \forall i \in I, J \le comap (Pi.evalMonoidHom M i) (S i) $$$

Lean4

@[to_additive]
theorem le_pi_iff {I : Set ι} {S : ∀ i, Submonoid (M i)} {J : Submonoid (∀ i, M i)} :
    J ≤ pi I S ↔ ∀ i ∈ I, J ≤ comap (Pi.evalMonoidHom M i) (S i) :=
  Set.subset_pi_iff

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