Theorems · Definition · general topology

RestrictedProduct.inclusion

{ι : Type u_1} →
  (R : ι → Type u_2) →
    (A : (i : ι) → Set (R i)) →
      {𝓕 𝓖 : Filter ι} →
        𝓕 ≤ 𝓖 → RestrictedProduct (fun i => R i) (fun i => A i) 𝓖 → RestrictedProduct (fun i => R i) (fun i => A i) 𝓕

If 𝓕 ≤ 𝓖, the restricted product Πʳ i, [R i, A i]_[𝓖] is naturally included in Πʳ i, [R i, A i]_[𝓕]. This is the corresponding map.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

21 results in Mathlib

Foundations

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