Theorems · Theorem · general topology

Filter.map_atTop_finsetSum_le_of_sum_eq

∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid 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 additive 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 ∈ 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

AddCommMonoid