Theorems · Theorem · general topology

Filter.map_atTop_finsetProd_le_of_prod_eq

∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] {f : α → M} {g : β → M},
  (∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    Filter.map (fun s => ∏ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∏ x ∈ s, g x) Filter.atTop

Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∏ b ∈ s, f b) with atTop.map (fun s ↦ ∏ b ∈ s, g b). This is useful to compare the set of limit points of Π b in s, f b as s → atTop with the similar set for g.

Defined in

Mathlib.Order.Filter.AtTopBot.BigOperators

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommMonoid