Theorems · Theorem · general topology

RestrictedProduct.ext

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

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

15 results in Mathlib

Foundations

Depth 9 from the axioms · uses Quot.sound