Theorems · Theorem · general topology

RestrictedProduct.range_inclusion

∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖),
  Set.range (RestrictedProduct.inclusion R A h) = {x | ∀ᶠ (i : ι) in 𝓖, x i ∈ A i}

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound