Mathlib.Order.Filter.Pi

Filter.tendsto_eval_pi theorem

(f : ∀ i, Filter (α i)) (i : ι) : Tendsto (eval i) (pi f) (f i)

Full source

theorem tendsto_eval_pi (f : ∀ i, Filter (α i)) (i : ι) : Tendsto (eval i) (pi f) (f i) :=
  tendsto_iInf' i tendsto_comap

Tendency of Evaluation Maps under Pi Filter

Informal description

For any family of filters $f_i$ on types $\alpha_i$ indexed by $i \in \iota$, and for any fixed index $i \in \iota$, the evaluation function $\operatorname{eval}_i$ tends to the filter $f_i$ when the domain is equipped with the pi filter $\operatorname{pi} f$. In other words, the evaluation map $\operatorname{eval}_i : (\forall i, \alpha_i) \to \alpha_i$ satisfies $\operatorname{Tendsto} (\operatorname{eval}_i) (\operatorname{pi} f) (f_i)$ for each $i \in \iota$.

Filter.tendsto_pi theorem

{β : Type*} {m : β → ∀ i, α i} {l : Filter β} : Tendsto m l (pi f) ↔ ∀ i, Tendsto (fun x => m x i) l (f i)

Full source

theorem tendsto_pi {β : Type*} {m : β → ∀ i, α i} {l : Filter β} :
    TendstoTendsto m l (pi f) ↔ ∀ i, Tendsto (fun x => m x i) l (f i) := by
  simp only [pi, tendsto_iInf, tendsto_comap_iff]; rfl

Characterization of Tendency to Pi Filter via Componentwise Tendency

Informal description

For a function $m : \beta \to \prod_i \alpha_i$ and a filter $l$ on $\beta$, the function $m$ tends to the pi filter $\prod_i f_i$ with respect to $l$ if and only if for every index $i$, the component function $x \mapsto m(x)_i$ tends to the filter $f_i$ with respect to $l$.

Filter.le_pi theorem

{g : Filter (∀ i, α i)} : g ≤ pi f ↔ ∀ i, Tendsto (eval i) g (f i)

Full source

theorem le_pi {g : Filter (∀ i, α i)} : g ≤ pi f ↔ ∀ i, Tendsto (eval i) g (f i) :=
  tendsto_pi

Characterization of Pi Filter Refinement via Componentwise Tendency

Informal description

For any filter $g$ on the product type $\prod_i \alpha_i$, the filter $g$ is finer than the pi filter $\prod_i f_i$ if and only if for every index $i$, the evaluation map $\operatorname{eval}_i$ tends to $f_i$ with respect to $g$. In other words, $g \leq \prod_i f_i$ if and only if for each $i$, $\operatorname{Tendsto} (\operatorname{eval}_i) g (f_i)$.

Filter.pi_mono theorem

(h : ∀ i, f₁ i ≤ f₂ i) : pi f₁ ≤ pi f₂

Full source

@[mono]
theorem pi_mono (h : ∀ i, f₁ i ≤ f₂ i) : pi f₁ ≤ pi f₂ :=
  iInf_mono fun i => comap_mono <| h i

Monotonicity of Pi Filter: $f_1(i) \leq f_2(i)$ implies $\prod_i f_1(i) \leq \prod_i f_2(i)$

Informal description

For any indexed family of filters $\{f_1(i)\}_{i \in \iota}$ and $\{f_2(i)\}_{i \in \iota}$ on types $\{\alpha_i\}_{i \in \iota}$, if $f_1(i) \leq f_2(i)$ for all $i \in \iota$, then the pi filter $\prod_i f_1(i)$ is less than or equal to the pi filter $\prod_i f_2(i)$.

Filter.mem_pi_of_mem theorem

(i : ι) {s : Set (α i)} (hs : s ∈ f i) : eval i ⁻¹' s ∈ pi f

Full source

theorem mem_pi_of_mem (i : ι) {s : Set (α i)} (hs : s ∈ f i) : evaleval i ⁻¹' seval i ⁻¹' s ∈ pi f :=
  mem_iInf_of_mem i <| preimage_mem_comap hs

Preimage of Filter Member Belongs to Pi Filter

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of filters on types $\{\alpha_i\}_{i \in \iota}$. For any index $i \in \iota$ and any set $s \subseteq \alpha_i$ that belongs to the filter $f_i$, the preimage of $s$ under the evaluation function at $i$ belongs to the pi filter $\prod_{i \in \iota} f_i$. In other words, if $s \in f_i$, then $\text{eval}_i^{-1}(s) \in \prod_{i \in \iota} f_i$.

Filter.pi_mem_pi theorem

{I : Set ι} (hI : I.Finite) (h : ∀ i ∈ I, s i ∈ f i) : I.pi s ∈ pi f

Full source

theorem pi_mem_pi {I : Set ι} (hI : I.Finite) (h : ∀ i ∈ I, s i ∈ f i) : I.pi s ∈ pi f := by
  rw [pi_def, biInter_eq_iInter]
  refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl
  exact preimage_mem_comap (h i i.2)

Membership of Finite Product in Pi Filter

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of filters on types $\{\alpha_i\}_{i \in \iota}$. For any finite subset $I \subseteq \iota$ and any family of sets $\{s_i\}_{i \in I}$ such that $s_i \in f_i$ for each $i \in I$, the product set $\prod_{i \in I} s_i$ belongs to the pi filter $\prod_{i \in \iota} f_i$.

Filter.mem_pi theorem

 {s : Set (∀ i, α i)} : s ∈ pi f ↔ ∃ I : Set ι, I.Finite ∧ ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s

Full source

theorem mem_pi {s : Set (∀ i, α i)} :
    s ∈ pi fs ∈ pi f ↔ ∃ I : Set ι, I.Finite ∧ ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s := by
  constructor
  · simp only [pi, mem_iInf', mem_comap, pi_def]
    rintro ⟨I, If, V, hVf, -, rfl, -⟩
    choose t htf htV using hVf
    exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
  · rintro ⟨I, If, t, htf, hts⟩
    exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

Characterization of Membership in Pi Filter via Finite Product Sets

Informal description

For any set $s$ of functions in $\prod_{i} \alpha_i$, $s$ belongs to the pi filter $\prod_{i} f_i$ if and only if there exists a finite subset $I \subseteq \iota$ and a family of sets $\{t_i\}_{i \in \iota}$ such that: 1. For each $i$, $t_i \in f_i$, and 2. The product set $\prod_{i \in I} t_i$ is contained in $s$.

Filter.mem_pi' theorem

 {s : Set (∀ i, α i)} : s ∈ pi f ↔ ∃ I : Finset ι, ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ Set.pi (↑I) t ⊆ s

Full source

theorem mem_pi' {s : Set (∀ i, α i)} :
    s ∈ pi fs ∈ pi f ↔ ∃ I : Finset ι, ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ Set.pi (↑I) t ⊆ s :=
  mem_pi.trans exists_finite_iff_finset

Characterization of Pi Filter Membership via Finite Index Subset

Informal description

For any set $s$ of functions in $\prod_{i} \alpha_i$, $s$ belongs to the pi filter $\prod_{i} f_i$ if and only if there exists a finite subset $I \subseteq \iota$ (represented as a finset) and a family of sets $\{t_i\}_{i \in \iota}$ such that: 1. For each $i$, $t_i \in f_i$, and 2. The product set $\prod_{i \in I} t_i$ is contained in $s$.

Filter.mem_of_pi_mem_pi theorem

[∀ i, NeBot (f i)] {I : Set ι} (h : I.pi s ∈ pi f) {i : ι} (hi : i ∈ I) : s i ∈ f i

Full source

theorem mem_of_pi_mem_pi [∀ i, NeBot (f i)] {I : Set ι} (h : I.pi s ∈ pi f) {i : ι} (hi : i ∈ I) :
    s i ∈ f i := by
  classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : updateupdate g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi

Component Membership in Pi Filter Implies Membership in Individual Filters

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of non-trivial filters on types $\{\alpha_i\}_{i \in \iota}$. For any subset $I \subseteq \iota$ and any family of sets $\{s_i \subseteq \alpha_i\}_{i \in \iota}$, if the product set $\prod_{i \in I} s_i$ belongs to the pi filter $\prod_{i} f_i$, then for every index $i \in I$, the set $s_i$ belongs to the filter $f_i$.

Filter.pi_mem_pi_iff theorem

[∀ i, NeBot (f i)] {I : Set ι} (hI : I.Finite) : I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i

Full source

@[simp]
theorem pi_mem_pi_iff [∀ i, NeBot (f i)] {I : Set ι} (hI : I.Finite) :
    I.pi s ∈ pi fI.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i :=
  ⟨fun h _i hi => mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩

Characterization of Pi Filter Membership via Finite Index Subset

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of non-trivial filters on types $\{\alpha_i\}_{i \in \iota}$. For any finite subset $I \subseteq \iota$ and any family of sets $\{s_i \subseteq \alpha_i\}_{i \in I}$, the product set $\prod_{i \in I} s_i$ belongs to the pi filter $\prod_{i} f_i$ if and only if for every $i \in I$, the set $s_i$ belongs to the filter $f_i$.

Filter.Eventually.eval_pi theorem

{i : ι} (hf : ∀ᶠ x : α i in f i, p i x) : ∀ᶠ x : ∀ i : ι, α i in pi f, p i (x i)

Full source

theorem Eventually.eval_pi {i : ι} (hf : ∀ᶠ x : α i in f i, p i x) :
    ∀ᶠ x : ∀ i : ι, α i in pi f, p i (x i) := (tendsto_eval_pi _ _).eventually hf

Eventual Property Preservation under Pi Filter Evaluation

Informal description

For any index $i \in \iota$ and any predicate $p_i : \alpha_i \to \text{Prop}$, if the set $\{x \mid p_i x\}$ belongs to the filter $f_i$, then the set $\{x \mid p_i (x i)\}$ belongs to the pi filter $\prod_{i} f_i$ on the product type $\forall i, \alpha_i$. In other words, if $p_i$ holds eventually in $f_i$, then $p_i$ holds eventually in the pi filter when evaluated at index $i$.

Filter.eventually_pi theorem

[Finite ι] (hf : ∀ i, ∀ᶠ x in f i, p i x) : ∀ᶠ x : ∀ i, α i in pi f, ∀ i, p i (x i)

Full source

theorem eventually_pi [Finite ι] (hf : ∀ i, ∀ᶠ x in f i, p i x) :
    ∀ᶠ x : ∀ i, α i in pi f, ∀ i, p i (x i) := eventually_all.2 fun _i => (hf _).eval_pi

Eventual Universal Quantifier Commutation with Pi Filter

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $f_i$ be a filter on a type $\alpha_i$ and $p_i : \alpha_i \to \text{Prop}$ be a predicate. If for every $i \in \iota$, the predicate $p_i$ holds eventually in $f_i$, then the predicate $\forall i, p_i (x i)$ holds eventually in the pi filter $\prod_{i} f_i$ on the product type $\forall i, \alpha_i$. In symbols: $$\left(\forall i, \forall^f x, p_i x\right) \implies \left(\forall^{\prod_i f_i} x, \forall i, p_i (x i)\right)$$

Filter.hasBasis_pi theorem

 {ι' : ι → Type*} {s : ∀ i, ι' i → Set (α i)} {p : ∀ i, ι' i → Prop} (h : ∀ i, (f i).HasBasis (p i) (s i)) :
  (pi f).HasBasis (fun If : Set ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If : Set ι × ∀ i, ι' i =>
    If.1.pi fun i => s i <| If.2 i

Full source

theorem hasBasis_pi {ι' : ι → Type*} {s : ∀ i, ι' i → Set (α i)} {p : ∀ i, ι' i → Prop}
    (h : ∀ i, (f i).HasBasis (p i) (s i)) :
    (pi f).HasBasis (fun If : SetSet ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))
      fun If : SetSet ι × ∀ i, ι' i => If.1.pi fun i => s i <| If.2 i := by
  simpa [Set.pi_def] using hasBasis_iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)

Basis Characterization of Pi Filter: $\prod_i f_i$ has basis of finite products of basis sets

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of filters on types $\{\alpha_i\}_{i \in \iota}$. Suppose for each $i \in \iota$, the filter $f_i$ has a basis consisting of sets $\{s_i(j)\}_{j \in \iota'_i}$ indexed by a predicate $p_i : \iota'_i \to \text{Prop}$. Then the pi filter $\prod_i f_i$ has a basis consisting of all finite product sets $\prod_{i \in I} s_i(j_i)$, where $I$ is a finite subset of $\iota$ and for each $i \in I$, $j_i \in \iota'_i$ satisfies $p_i(j_i)$. More precisely, a set $S$ belongs to $\prod_i f_i$ if and only if there exists a finite subset $I \subseteq \iota$ and for each $i \in I$ an index $j_i \in \iota'_i$ satisfying $p_i(j_i)$, such that $\prod_{i \in I} s_i(j_i) \subseteq S$.

Filter.hasBasis_pi_same_index theorem

 {κ : Type*} {p : κ → Prop} {s : Π i : ι, κ → Set (α i)} (h : ∀ i : ι, (f i).HasBasis p (s i))
  (h_dir : ∀ I : Set ι, ∀ k : ι → κ, I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)) :
  (pi f).HasBasis (fun Ik : Set ι × κ ↦ Ik.1.Finite ∧ p Ik.2) (fun Ik ↦ Ik.1.pi (fun i ↦ s i Ik.2))

Full source

theorem hasBasis_pi_same_index {κ : Type*} {p : κ → Prop} {s : Π i : ι, κ → Set (α i)}
    (h : ∀ i : ι, (f i).HasBasis p (s i))
    (h_dir : ∀ I : Set ι, ∀ k : ι → κ, I.Finite → (∀ i ∈ I, p (k i)) →
      ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)) :
    (pi f).HasBasis (fun Ik : SetSet ι × κ ↦ Ik.1.Finite ∧ p Ik.2)
      (fun Ik ↦ Ik.1.pi (fun i ↦ s i Ik.2)) := by
  refine hasBasis_pi h |>.to_hasBasis ?_ ?_
  · rintro ⟨I, k⟩ ⟨hI, hk⟩
    rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
    exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩
  · rintro ⟨I, k⟩ ⟨hI, hk⟩
    exact ⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩

Basis Characterization of Pi Filter with Common Index Type

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of filters on types $\{\alpha_i\}_{i \in \iota}$. Suppose each filter $f_i$ has a basis consisting of sets $\{s_i(k)\}_{k \in \kappa}$ indexed by a predicate $p : \kappa \to \text{Prop}$, where $\kappa$ is a common index type. Assume further that for any finite subset $I \subseteq \iota$ and any family of indices $\{k_i\}_{i \in I}$ with $p(k_i)$ for each $i \in I$, there exists an index $k_0 \in \kappa$ such that $p(k_0)$ holds and $s_i(k_0) \subseteq s_i(k_i)$ for all $i \in I$. Then the pi filter $\prod_i f_i$ has a basis consisting of all finite product sets $\prod_{i \in I} s_i(k)$, where $I$ is a finite subset of $\iota$ and $k \in \kappa$ satisfies $p(k)$.

Filter.HasBasis.pi_self theorem

 {α : Type*} {κ : Type*} {f : Filter α} {p : κ → Prop} {s : κ → Set α} (h : f.HasBasis p s) :
  (pi fun _ ↦ f).HasBasis (fun Ik : Set ι × κ ↦ Ik.1.Finite ∧ p Ik.2) (fun Ik ↦ Ik.1.pi (fun _ ↦ s Ik.2))

Full source

theorem HasBasis.pi_self {α : Type*} {κ : Type*} {f : Filter α} {p : κ → Prop} {s : κ → Set α}
    (h : f.HasBasis p s) :
    (pi fun _ ↦ f).HasBasis (fun Ik : SetSet ι × κ ↦ Ik.1.Finite ∧ p Ik.2)
      (fun Ik ↦ Ik.1.pi (fun _ ↦ s Ik.2)) := by
  refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)
  rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi))
    with ⟨k₀, hk₀, hk₀'⟩
  exact ⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩

Basis characterization of pi filter with identical factors: $\prod_{i \in \iota} f$ has basis of finite products of basis sets from $f$

Informal description

Let $f$ be a filter on a type $\alpha$ with a basis consisting of sets $\{s(k)\}_{k \in \kappa}$ indexed by a predicate $p : \kappa \to \text{Prop}$. Then the pi filter $\prod_{i \in \iota} f$ (where the same filter $f$ is used for each index $i$) has a basis consisting of all finite product sets $\prod_{i \in I} s(k)$, where $I$ is a finite subset of the index set $\iota$ and $k \in \kappa$ satisfies $p(k)$.

Filter.le_pi_principal theorem

(s : (i : ι) → Set (α i)) : 𝓟 (univ.pi s) ≤ pi fun i ↦ 𝓟 (s i)

Full source

theorem le_pi_principal (s : (i : ι) → Set (α i)) :
    𝓟 (univ.pi s) ≤ pi fun i ↦ 𝓟 (s i) :=
  le_pi.2 fun i ↦ tendsto_principal_principal.2 fun _f hf ↦ hf i trivial

Principal Filter of Product Set is Finer than Pi Filter of Principal Filters

Informal description

For any family of sets $s_i \subseteq \alpha_i$ indexed by $i \in \iota$, the principal filter generated by the product set $\prod_{i \in \iota} s_i$ is finer than the pi filter of the principal filters generated by each $s_i$. In other words: \[ \mathcal{P}\left(\prod_{i \in \iota} s_i\right) \leq \prod_{i \in \iota} \mathcal{P}(s_i) \]

Filter.pi_principal theorem

[Finite ι] (s : (i : ι) → Set (α i)) : pi (fun i ↦ 𝓟 (s i)) = 𝓟 (univ.pi s)

Full source

/-- The indexed product of finitely many principal filters
is the principal filter corresponding to the cylinder `Set.univ.pi s`.

If the index type is infinite, then `mem_pi_principal` and `hasBasis_pi_principal` may be useful. -/
@[simp]
theorem pi_principal [Finite ι] (s : (i : ι) → Set (α i)) :
    pi (fun i ↦ 𝓟 (s i)) = 𝓟 (univ.pi s) := by
  simp [Filter.pi, Set.pi_def]

Pi Filter of Principal Filters Equals Principal Filter of Product Set for Finite Index

Informal description

For a finite index type $\iota$ and a family of sets $s_i \subseteq \alpha_i$ for each $i \in \iota$, the pi filter of the principal filters generated by $s_i$ is equal to the principal filter generated by the product set $\prod_{i \in \iota} s_i$. In symbols: \[ \prod_{i \in \iota} \mathcal{P}(s_i) = \mathcal{P}\left(\prod_{i \in \iota} s_i\right) \]

Filter.mem_pi_principal theorem

{t : Set ((i : ι) → α i)} : t ∈ pi (fun i ↦ 𝓟 (s i)) ↔ ∃ I : Set ι, I.Finite ∧ I.pi s ⊆ t

Full source

/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters
is a pricipal filter, see `pi_principal`. -/
theorem mem_pi_principal {t : Set ((i : ι) → α i)} :
    t ∈ pi (fun i ↦ 𝓟 (s i))t ∈ pi (fun i ↦ 𝓟 (s i)) ↔ ∃ I : Set ι, I.Finite ∧ I.pi s ⊆ t :=
  (hasBasis_pi (fun i ↦ hasBasis_principal _)).mem_iff.trans <| by simp

Membership Criterion for Pi Filter of Principal Filters: $t \in \prod_i \mathcal{P}(s_i) \iff \exists$ finite $I \subseteq \iota$ with $\prod_{i \in I} s_i \subseteq t$

Informal description

For any set $t$ of functions from an index type $\iota$ to $\alpha_i$, $t$ belongs to the pi filter of principal filters generated by sets $s_i \subseteq \alpha_i$ if and only if there exists a finite subset $I \subseteq \iota$ such that the product set $\prod_{i \in I} s_i$ is contained in $t$.

Filter.hasBasis_pi_principal theorem

(s : (i : ι) → Set (α i)) : HasBasis (pi fun i ↦ 𝓟 (s i)) Set.Finite (Set.pi · s)

Full source

/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters
is a pricipal filter, see `pi_principal`. -/
theorem hasBasis_pi_principal (s : (i : ι) → Set (α i)) :
    HasBasis (pi fun i ↦ 𝓟 (s i)) Set.Finite (Set.pi · s) :=
  ⟨fun _ ↦ mem_pi_principal⟩

Basis of Pi Filter of Principal Filters via Finite Products

Informal description

For a family of sets $s_i \subseteq \alpha_i$ indexed by $i \in \iota$, the pi filter $\prod_i \mathcal{P}(s_i)$ has a basis consisting of finite product sets $\prod_{i \in I} s_i$ where $I$ is a finite subset of $\iota$. More precisely, a set $t$ belongs to $\prod_i \mathcal{P}(s_i)$ if and only if there exists a finite subset $I \subseteq \iota$ such that $\prod_{i \in I} s_i \subseteq t$.

Filter.pi_pure theorem

[Finite ι] (f : (i : ι) → α i) : pi (pure <| f ·) = pure f

Full source

/-- The indexed product of finitely many pure filters `pure (f i)` is the pure filter `pure f`.

If the index type is infinite, then `mem_pi_pure` and `hasBasis_pi_pure` below may be useful. -/
@[simp]
theorem pi_pure [Finite ι] (f : (i : ι) → α i) : pi (pure <| f ·) = pure f := by
  simp only [← principal_singleton, pi_principal, univ_pi_singleton]

Pi Filter of Pure Elements Equals Pure Function for Finite Index

Informal description

For a finite index type $\iota$ and a family of elements $f_i \in \alpha_i$ for each $i \in \iota$, the pi filter of the pure filters generated by $f_i$ is equal to the pure filter generated by the function $f = (f_i)_{i \in \iota}$. In symbols: \[ \prod_{i \in \iota} \text{pure}(f_i) = \text{pure}(f) \]

Filter.mem_pi_pure theorem

 {f : (i : ι) → α i} {s : Set ((i : ι) → α i)} :
  s ∈ pi (fun i ↦ pure (f i)) ↔ ∃ I : Set ι, I.Finite ∧ ∀ g, (∀ i ∈ I, g i = f i) → g ∈ s

Full source

/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`. -/
theorem mem_pi_pure {f : (i : ι) → α i} {s : Set ((i : ι) → α i)} :
    s ∈ pi (fun i ↦ pure (f i))s ∈ pi (fun i ↦ pure (f i)) ↔ ∃ I : Set ι, I.Finite ∧ ∀ g, (∀ i ∈ I, g i = f i) → g ∈ s := by
  simp only [← principal_singleton, mem_pi_principal]
  simp [subset_def]

Membership in Pi Filter of Pure Filters via Finite Agreement

Informal description

For a family of functions $f : \forall i, \alpha_i$ and a set $s$ of functions, $s$ belongs to the pi filter of the family of pure filters $\text{pure}(f_i)$ if and only if there exists a finite subset $I \subseteq \iota$ such that any function $g$ that agrees with $f$ on $I$ is in $s$. In other words, $s \in \prod_i \text{pure}(f_i) \leftrightarrow \exists I \subseteq \iota \text{ finite}, \forall g, (\forall i \in I, g(i) = f(i)) \rightarrow g \in s$.

Filter.hasBasis_pi_pure theorem

(f : (i : ι) → α i) : HasBasis (pi fun i ↦ pure (f i)) Set.Finite (fun I ↦ {g | ∀ i ∈ I, g i = f i})

Full source

/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`. -/
theorem hasBasis_pi_pure (f : (i : ι) → α i) :
    HasBasis (pi fun i ↦ pure (f i)) Set.Finite (fun I ↦ {g | ∀ i ∈ I, g i = f i}) :=
  ⟨fun _ ↦ mem_pi_pure⟩

Basis Characterization of Pi Filter of Pure Functions via Finite Agreement

Informal description

For a family of functions $f : \forall i, \alpha_i$, the pi filter $\prod_i \text{pure}(f_i)$ has a basis consisting of sets $\{g \mid \forall i \in I, g(i) = f(i)\}$ indexed by finite subsets $I \subseteq \iota$. In other words, a set $s$ is in $\prod_i \text{pure}(f_i)$ if and only if there exists a finite subset $I \subseteq \iota$ such that any function $g$ that agrees with $f$ on $I$ is in $s$.

Filter.pi_inf_principal_univ_pi_eq_bot theorem

: pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥

Full source

@[simp]
theorem pi_inf_principal_univ_pi_eq_bot :
    pipi f ⊓ 𝓟 (Set.pi univ s)pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥ := by
  constructor
  · simp only [inf_principal_eq_bot, mem_pi]
    contrapose!
    rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
    have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
    choose x hxs hxt using this
    exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
  · simp only [inf_principal_eq_bot]
    rintro ⟨i, hi⟩
    filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial

Bottom Filter Condition for Pi Filter Intersected with Universal Product Principal Filter

Informal description

For a family of filters $\{f_i\}_{i \in \iota}$ on types $\{\alpha_i\}_{i \in \iota}$ and a family of sets $\{s_i \subseteq \alpha_i\}_{i \in \iota}$, the infimum of the pi filter $\prod_{i} f_i$ and the principal filter generated by the universal product set $\prod_{i} s_i$ is the bottom filter if and only if there exists an index $i$ such that the infimum of $f_i$ and the principal filter generated by $s_i$ is the bottom filter. In other words, $\prod_{i} f_i \sqcap \mathcal{P}(\prod_{i} s_i) = \bot$ if and only if $\exists i, f_i \sqcap \mathcal{P}(s_i) = \bot$.

Filter.pi_inf_principal_pi_eq_bot theorem

[∀ i, NeBot (f i)] {I : Set ι} : pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Full source

@[simp]
theorem pi_inf_principal_pi_eq_bot [∀ i, NeBot (f i)] {I : Set ι} :
    pipi f ⊓ 𝓟 (Set.pi I s)pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥ := by
  classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

Bottom Filter Condition for Product Filter Intersected with Principal Filter on Indexed Product Set

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of non-trivial filters on types $\{\alpha_i\}_{i \in \iota}$, and let $I \subseteq \iota$ be a subset of indices. For any family of sets $\{s_i \subseteq \alpha_i\}_{i \in \iota}$, the infimum of the product filter $\prod_{i} f_i$ and the principal filter generated by the product set $\prod_{i \in I} s_i$ is the bottom filter if and only if there exists an index $i \in I$ such that the infimum of $f_i$ and the principal filter generated by $s_i$ is the bottom filter. In other words, $\prod_{i} f_i \sqcap \mathcal{P}(\prod_{i \in I} s_i) = \bot$ if and only if $\exists i \in I, f_i \sqcap \mathcal{P}(s_i) = \bot$.

Filter.pi_inf_principal_univ_pi_neBot theorem

: NeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ i, NeBot (f i ⊓ 𝓟 (s i))

Full source

@[simp]
theorem pi_inf_principal_univ_pi_neBot :
    NeBotNeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ i, NeBot (f i ⊓ 𝓟 (s i)) := by simp [neBot_iff]

Non-triviality of Product Filter Intersected with Principal Filter on Universal Product Set

Informal description

The filter $\text{pi } f \sqcap \mathcal{P}(\prod_{i \in \text{univ}} s_i)$ is non-trivial if and only if for every index $i$, the filter $f_i \sqcap \mathcal{P}(s_i)$ is non-trivial. Here, $\text{pi } f$ denotes the product filter of the family $f$, $\mathcal{P}$ denotes the principal filter, $\prod_{i \in \text{univ}} s_i$ is the product of sets $s_i$ over all indices $i$, and $\sqcap$ denotes the infimum of filters.

Filter.pi_inf_principal_pi_neBot theorem

[∀ i, NeBot (f i)] {I : Set ι} : NeBot (pi f ⊓ 𝓟 (I.pi s)) ↔ ∀ i ∈ I, NeBot (f i ⊓ 𝓟 (s i))

Full source

@[simp]
theorem pi_inf_principal_pi_neBot [∀ i, NeBot (f i)] {I : Set ι} :
    NeBotNeBot (pi f ⊓ 𝓟 (I.pi s)) ↔ ∀ i ∈ I, NeBot (f i ⊓ 𝓟 (s i)) := by simp [neBot_iff]

Non-triviality of Pi Filter Intersected with Principal Filter on Product Set

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of non-trivial filters on types $\{\alpha_i\}_{i \in \iota}$, and let $I \subseteq \iota$ be a subset of indices. For any family of sets $\{s_i \subseteq \alpha_i\}_{i \in \iota}$, the filter $\text{pi } f \sqcap \mathcal{P}(\prod_{i \in I} s_i)$ is non-trivial if and only if for every $i \in I$, the filter $f_i \sqcap \mathcal{P}(s_i)$ is non-trivial.

Filter.PiInfPrincipalPi.neBot instance

[h : ∀ i, NeBot (f i ⊓ 𝓟 (s i))] {I : Set ι} : NeBot (pi f ⊓ 𝓟 (I.pi s))

Full source

instance PiInfPrincipalPi.neBot [h : ∀ i, NeBot (f i ⊓ 𝓟 (s i))] {I : Set ι} :
    NeBot (pipi f ⊓ 𝓟 (I.pi s)) :=
  (pi_inf_principal_univ_pi_neBot.2 ‹_›).mono <|
    inf_le_inf_left _ <| principal_mono.2 fun _ hx i _ => hx i trivial

Non-triviality of Product Filter Intersected with Principal Filter on Indexed Product Set

Informal description

For any indexed family of filters $f_i$ on types $\alpha_i$ and sets $s_i \subseteq \alpha_i$, if for each index $i$ the filter $f_i \sqcap \mathcal{P}(s_i)$ is non-trivial, then the filter $\text{pi } f \sqcap \mathcal{P}(\prod_{i \in I} s_i)$ is also non-trivial for any subset of indices $I \subseteq \iota$. Here, $\text{pi } f$ denotes the product filter of the family $f$, $\mathcal{P}$ denotes the principal filter, and $\prod_{i \in I} s_i$ is the product of sets $s_i$ over indices $i \in I$.

Filter.pi_eq_bot theorem

: pi f = ⊥ ↔ ∃ i, f i = ⊥

Full source

@[simp]
theorem pi_eq_bot : pipi f = ⊥ ↔ ∃ i, f i = ⊥ := by
  simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ

Product Filter is Bottom if and Only if a Component is Bottom

Informal description

The product filter $\prod_i f_i$ on the dependent function space $\prod_i \alpha_i$ is the bottom filter if and only if there exists an index $i$ such that the filter $f_i$ on $\alpha_i$ is the bottom filter.

Filter.pi_neBot theorem

: NeBot (pi f) ↔ ∀ i, NeBot (f i)

Full source

@[simp]
theorem pi_neBot : NeBotNeBot (pi f) ↔ ∀ i, NeBot (f i) := by simp [neBot_iff]

Non-triviality of Pi Filter: $\text{pi } f \neq \bot \leftrightarrow \forall i, f_i \neq \bot$

Informal description

The pi filter $\text{pi } f$ on the product type $\forall i, \alpha_i$ is non-trivial if and only if for every index $i$, the filter $f_i$ on $\alpha_i$ is non-trivial.

Filter.instNeBotForallPi instance

[∀ i, NeBot (f i)] : NeBot (pi f)

Full source

instance [∀ i, NeBot (f i)] : NeBot (pi f) :=
  pi_neBot.2 ‹_›

Non-triviality of Pi Filter from Non-trivial Components

Informal description

For any family of filters $f_i$ on types $\alpha_i$ where each $f_i$ is non-trivial, the pi filter $\text{pi } f$ on the product type $\forall i, \alpha_i$ is also non-trivial.

Filter.map_eval_pi theorem

(f : ∀ i, Filter (α i)) [∀ i, NeBot (f i)] (i : ι) : map (eval i) (pi f) = f i

Full source

@[simp]
theorem map_eval_pi (f : ∀ i, Filter (α i)) [∀ i, NeBot (f i)] (i : ι) :
    map (eval i) (pi f) = f i := by
  refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_
  rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
  rw [← image_subset_iff] at hI
  refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)
  exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)

Image of Evaluation Map under Pi Filter Equals Component Filter

Informal description

For any family of non-trivial filters $f_i$ on types $\alpha_i$ indexed by $i \in \iota$, and for any fixed index $i \in \iota$, the image filter of the evaluation map $\operatorname{eval}_i$ under the pi filter $\operatorname{pi} f$ is equal to $f_i$. In other words: \[ \operatorname{map} (\operatorname{eval}_i) (\operatorname{pi} f) = f_i. \]

Filter.pi_le_pi theorem

[∀ i, NeBot (f₁ i)] : pi f₁ ≤ pi f₂ ↔ ∀ i, f₁ i ≤ f₂ i

Full source

@[simp]
theorem pi_le_pi [∀ i, NeBot (f₁ i)] : pipi f₁ ≤ pi f₂ ↔ ∀ i, f₁ i ≤ f₂ i :=
  ⟨fun h i => map_eval_pi f₁ i ▸ (tendsto_eval_pi _ _).mono_left h, pi_mono⟩

Comparison of Pi Filters: $\prod_i f_1(i) \leq \prod_i f_2(i) \leftrightarrow \forall i, f_1(i) \leq f_2(i)$

Informal description

For any indexed family of non-trivial filters $\{f_1(i)\}_{i \in \iota}$ and $\{f_2(i)\}_{i \in \iota}$ on types $\{\alpha_i\}_{i \in \iota}$, the pi filter $\prod_i f_1(i)$ is less than or equal to the pi filter $\prod_i f_2(i)$ if and only if $f_1(i) \leq f_2(i)$ for all $i \in \iota$.

Filter.pi_inj theorem

[∀ i, NeBot (f₁ i)] : pi f₁ = pi f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem pi_inj [∀ i, NeBot (f₁ i)] : pipi f₁ = pi f₂ ↔ f₁ = f₂ := by
  refine ⟨fun h => ?_, congr_arg pi⟩
  have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
  haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
  exact hle.antisymm (pi_le_pi.1 h.ge)

Injectivity of Pi Filter Construction for Non-trivial Filters

Informal description

For any indexed family of non-trivial filters $\{f_1(i)\}_{i \in \iota}$ and $\{f_2(i)\}_{i \in \iota}$ on types $\{\alpha_i\}_{i \in \iota}$, the pi filters $\prod_i f_1(i)$ and $\prod_i f_2(i)$ are equal if and only if $f_1(i) = f_2(i)$ for all $i \in \iota$.

Filter.tendsto_piMap_pi theorem

 {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (α i)} {l' : ∀ i, Filter (β i)}
  (h : ∀ i, Tendsto (f i) (l i) (l' i)) : Tendsto (Pi.map f) (pi l) (pi l')

Full source

theorem tendsto_piMap_pi {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (α i)}
    {l' : ∀ i, Filter (β i)} (h : ∀ i, Tendsto (f i) (l i) (l' i)) :
    Tendsto (Pi.map f) (pi l) (pi l') :=
  tendsto_pi.2 fun i ↦ (h i).comp (tendsto_eval_pi _ _)

Component-wise Mapping Preserves Tendency to Pi Filters

Informal description

Let $\{ \alpha_i \}_{i \in \iota}$ and $\{ \beta_i \}_{i \in \iota}$ be families of types, and for each $i \in \iota$, let $f_i : \alpha_i \to \beta_i$ be a function between these types. Suppose for each $i \in \iota$ we have filters $l_i$ on $\alpha_i$ and $l'_i$ on $\beta_i$, such that $f_i$ tends to $l'_i$ with respect to $l_i$ (i.e., $\text{Tendsto } f_i l_i l'_i$ holds for each $i$). Then the component-wise mapping function $\text{Pi.map } f : (\forall i, \alpha_i) \to (\forall i, \beta_i)$ tends to the pi filter $\prod_i l'_i$ with respect to the pi filter $\prod_i l_i$.

Filter.coprodᵢ definition

(f : ∀ i, Filter (α i)) : Filter (∀ i, α i)

Full source

/-- Coproduct of filters. -/
protected def coprodᵢ (f : ∀ i, Filter (α i)) : Filter (∀ i, α i) :=
  ⨆ i : ι, comap (eval i) (f i)

Indexed coproduct filter

Informal description

The coproduct filter $\coprod_i f_i$ on the product type $\forall i, \alpha_i$ is defined as the supremum of the preimage filters $\text{comap}(\text{eval}_i)(f_i)$ for each index $i$, where $\text{eval}_i$ is the evaluation function at index $i$. A set $s$ belongs to $\coprod_i f_i$ if and only if for every index $i$, there exists a set $t_i \in f_i$ such that the preimage of $t_i$ under the evaluation function $\text{eval}_i$ is contained in $s$.

Filter.mem_coprodᵢ_iff theorem

{s : Set (∀ i, α i)} : s ∈ Filter.coprodᵢ f ↔ ∀ i : ι, ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s

Full source

theorem mem_coprodᵢ_iff {s : Set (∀ i, α i)} :
    s ∈ Filter.coprodᵢ fs ∈ Filter.coprodᵢ f ↔ ∀ i : ι, ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s := by simp [Filter.coprodᵢ]

Characterization of Membership in Indexed Coproduct Filter

Informal description

A set $s$ belongs to the indexed coproduct filter $\coprod_i f_i$ if and only if for every index $i$, there exists a set $t_i \in f_i$ such that the preimage of $t_i$ under the evaluation function $\text{eval}_i$ is contained in $s$.

Filter.compl_mem_coprodᵢ theorem

{s : Set (∀ i, α i)} : sᶜ ∈ Filter.coprodᵢ f ↔ ∀ i, (eval i '' s)ᶜ ∈ f i

Full source

theorem compl_mem_coprodᵢ {s : Set (∀ i, α i)} :
    sᶜsᶜ ∈ Filter.coprodᵢ fsᶜ ∈ Filter.coprodᵢ f ↔ ∀ i, (eval i '' s)ᶜ ∈ f i := by
  simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]

Complement Membership in Indexed Coproduct Filter via Image Complements

Informal description

For any set $s$ in the product space $\prod_i \alpha_i$, the complement $s^c$ belongs to the indexed coproduct filter $\coprod_i f_i$ if and only if for every index $i$, the complement of the image of $s$ under the evaluation map $\text{eval}_i$ belongs to the filter $f_i$. In other words: $$ s^c \in \coprod_i f_i \iff \forall i, (\text{eval}_i(s))^c \in f_i. $$

Filter.coprodᵢ_neBot_iff' theorem

: NeBot (Filter.coprodᵢ f) ↔ (∀ i, Nonempty (α i)) ∧ ∃ d, NeBot (f d)

Full source

theorem coprodᵢ_neBot_iff' :
    NeBotNeBot (Filter.coprodᵢ f) ↔ (∀ i, Nonempty (α i)) ∧ ∃ d, NeBot (f d) := by
  simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']

Non-triviality Condition for Indexed Coproduct Filter

Informal description

The indexed coproduct filter $\coprod_i f_i$ is non-trivial if and only if for every index $i$, the type $\alpha_i$ is nonempty, and there exists at least one index $d$ such that the filter $f_d$ is non-trivial.

Filter.coprodᵢ_neBot_iff theorem

[∀ i, Nonempty (α i)] : NeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d)

Full source

@[simp]
theorem coprodᵢ_neBot_iff [∀ i, Nonempty (α i)] : NeBotNeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d) := by
  simp [coprodᵢ_neBot_iff', *]

Non-triviality of Indexed Coproduct Filter

Informal description

For a family of types $\alpha_i$ where each $\alpha_i$ is nonempty, the coproduct filter $\coprod_i f_i$ on the product type $\forall i, \alpha_i$ is non-trivial if and only if there exists an index $d$ such that the filter $f_d$ is non-trivial.

Filter.coprodᵢ_eq_bot_iff' theorem

: Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥

Full source

theorem coprodᵢ_eq_bot_iff' : Filter.coprodᵢFilter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥ := by
  simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff]
    using coprodᵢ_neBot_iff'.not

Coproduct Filter is Bottom iff Empty Type or Trivial Filters

Informal description

The coproduct filter $\coprod_i f_i$ is equal to the bottom filter $\bot$ if and only if either there exists an index $i$ such that the type $\alpha_i$ is empty, or the family of filters $f$ is identically equal to $\bot$.

Filter.coprodᵢ_eq_bot_iff theorem

[∀ i, Nonempty (α i)] : Filter.coprodᵢ f = ⊥ ↔ f = ⊥

Full source

@[simp]
theorem coprodᵢ_eq_bot_iff [∀ i, Nonempty (α i)] : Filter.coprodᵢFilter.coprodᵢ f = ⊥ ↔ f = ⊥ := by
  simpa [funext_iff] using coprodᵢ_neBot_iff.not

Coproduct Filter is Bottom if and only if All Component Filters are Bottom

Informal description

For a family of nonempty types $\alpha_i$ and a family of filters $f_i$ on $\alpha_i$, the coproduct filter $\coprod_i f_i$ on the product type $\forall i, \alpha_i$ is equal to the bottom filter $\bot$ if and only if the family of filters $f_i$ is identically equal to the bottom filter (i.e., $f_i = \bot$ for all $i$).

Filter.coprodᵢ_bot' theorem

: Filter.coprodᵢ (⊥ : ∀ i, Filter (α i)) = ⊥

Full source

@[simp] theorem coprodᵢ_bot' : Filter.coprodᵢ (⊥ : ∀ i, Filter (α i)) = ⊥ :=
  coprodᵢ_eq_bot_iff'.2 (Or.inr rfl)

Coproduct of Bottom Filters is Bottom

Informal description

The coproduct filter $\coprod_i \bot$ of the family of bottom filters on $\alpha_i$ is equal to the bottom filter $\bot$.

Filter.coprodᵢ_bot theorem

: Filter.coprodᵢ (fun _ => ⊥ : ∀ i, Filter (α i)) = ⊥

Full source

@[simp]
theorem coprodᵢ_bot : Filter.coprodᵢ (fun _ => ⊥ : ∀ i, Filter (α i)) = ⊥ :=
  coprodᵢ_bot'

Coproduct of Constant Bottom Filters is Bottom

Informal description

The coproduct filter $\coprod_i \bot$ on the product type $\Pi_i \alpha_i$, where each component filter is the bottom filter $\bot$, is equal to the bottom filter $\bot$.

Filter.NeBot.coprodᵢ theorem

[∀ i, Nonempty (α i)] {i : ι} (h : NeBot (f i)) : NeBot (Filter.coprodᵢ f)

Full source

theorem NeBot.coprodᵢ [∀ i, Nonempty (α i)] {i : ι} (h : NeBot (f i)) : NeBot (Filter.coprodᵢ f) :=
  coprodᵢ_neBot_iff.2 ⟨i, h⟩

Non-triviality of Indexed Coproduct Filter from Non-trivial Component

Informal description

For a family of nonempty types $\alpha_i$ indexed by $i \in \iota$, if the filter $f_i$ on $\alpha_i$ is non-trivial for some index $i$, then the indexed coproduct filter $\coprod_i f_i$ on the product type $\Pi_i \alpha_i$ is also non-trivial.

Filter.coprodᵢ_neBot theorem

[∀ i, Nonempty (α i)] [Nonempty ι] (f : ∀ i, Filter (α i)) [H : ∀ i, NeBot (f i)] : NeBot (Filter.coprodᵢ f)

Full source

@[instance]
theorem coprodᵢ_neBot [∀ i, Nonempty (α i)] [Nonempty ι] (f : ∀ i, Filter (α i))
    [H : ∀ i, NeBot (f i)] : NeBot (Filter.coprodᵢ f) :=
  (H (Classical.arbitrary ι)).coprodᵢ

Non-triviality of Indexed Coproduct Filter from Non-trivial Components

Informal description

For a family of nonempty types $\alpha_i$ indexed by a nonempty set $\iota$, if for each $i \in \iota$ the filter $f_i$ on $\alpha_i$ is non-trivial, then the indexed coproduct filter $\coprod_i f_i$ on the product type $\Pi_i \alpha_i$ is also non-trivial.

Filter.coprodᵢ_mono theorem

(hf : ∀ i, f₁ i ≤ f₂ i) : Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂

Full source

@[mono]
theorem coprodᵢ_mono (hf : ∀ i, f₁ i ≤ f₂ i) : Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂ :=
  iSup_mono fun i => comap_mono (hf i)

Monotonicity of Indexed Coproduct Filter: $f_1(i) \leq f_2(i) \Rightarrow \coprod_i f_1(i) \leq \coprod_i f_2(i)$

Informal description

For any family of filters $(f_1(i))_{i \in I}$ and $(f_2(i))_{i \in I}$ on types $(\alpha_i)_{i \in I}$, if $f_1(i) \leq f_2(i)$ for every index $i \in I$, then the coproduct filter $\coprod_i f_1(i)$ is less than or equal to the coproduct filter $\coprod_i f_2(i)$ on the product type $\Pi_{i \in I} \alpha_i$.

Filter.map_pi_map_coprodᵢ_le theorem

: map (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)

Full source

theorem map_pi_map_coprodᵢ_le :
    map (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) ≤
      Filter.coprodᵢ fun i => map (m i) (f i) := by
  simp only [le_def, mem_map, mem_coprodᵢ_iff]
  intro s h i
  obtain ⟨t, H, hH⟩ := h i
  exact ⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩

Inequality for Mapping Coproduct Filters Pointwise

Informal description

For a family of functions $m_i : \alpha_i \to \beta_i$ and a family of filters $f_i$ on $\alpha_i$, the image under the pointwise mapping $(k_i)_{i \in I} \mapsto (m_i(k_i))_{i \in I}$ of the coproduct filter $\coprod_i f_i$ is contained in the coproduct filter $\coprod_i \text{map}(m_i, f_i)$. In other words, the following inequality holds between filters on $\prod_i \beta_i$: \[ \text{map}\left((k_i)_{i \in I} \mapsto (m_i(k_i))_{i \in I}\right) \left(\coprod_i f_i\right) \leq \coprod_i \text{map}(m_i, f_i). \]

Filter.Tendsto.pi_map_coprodᵢ theorem

 {g : ∀ i, Filter (β i)} (h : ∀ i, Tendsto (m i) (f i) (g i)) :
  Tendsto (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)

Full source

theorem Tendsto.pi_map_coprodᵢ {g : ∀ i, Filter (β i)} (h : ∀ i, Tendsto (m i) (f i) (g i)) :
    Tendsto (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g) :=
  map_pi_map_coprodᵢ_le.trans (coprodᵢ_mono h)

Tendency of Pointwise Mapping to Preserve Coproduct Filters

Informal description

For a family of functions $m_i : \alpha_i \to \beta_i$ and a family of filters $g_i$ on $\beta_i$, if for each index $i$ the function $m_i$ tends to $g_i$ with respect to the filters $f_i$ and $g_i$ (i.e., $\text{Tendsto } m_i f_i g_i$ holds), then the pointwise mapping $(k_i)_{i \in I} \mapsto (m_i(k_i))_{i \in I}$ tends to the coproduct filter $\coprod_i g_i$ with respect to the coproduct filter $\coprod_i f_i$ on the product type $\prod_i \alpha_i$.