Theorems · Theorem · general topology

RestrictedProduct.ext_iff

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι}
  {x y : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕}, x = y ↔ ∀ (i : ι), x i = y i

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses Quot.sound