Theorems · Theorem · general topology

RestrictedProduct.add_apply

∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Add (R i)] [inst_2 : ∀ (i : ι), AddMemClass (S i) (R i)]
  (x y : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (x + y) i = x i + y i

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SetLikeAddAddMemClass