le_pi_iff — Mathlib

English

For indexed subgroups, J ≤ pi I H iff each i ∈ I satisfies J ≤ comap (Pi.evalMonoidHom f i) (H i).

Русский

Для индекстируемых подгрупп J ≤ pi I H тогда и только если для каждого i ∈ I выполняется J ≤ comap (Pi.evalMonoidHom f i) (H i).

LaTeX

$$$ J \le \pi I H \iff \forall i \in I, J \le \mathrm{comap}(\Pi.evalMonoidHom f i)(H i) $$$

Lean4

@[to_additive]
theorem le_pi_iff {I : Set η} {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    J ≤ pi I H ↔ ∀ i ∈ I, J ≤ comap (Pi.evalMonoidHom f i) (H i) :=
  Set.subset_pi_iff

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