Theorems · Theorem · group theory

AddSubgroup.mem_pi

∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)}
  {p : (i : η) → f i}, p ∈ AddSubgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

5 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

AddGroup