English
If g is injective and f vanishes outside the range of g, then the two pushforwards of the atTop filter by finite products coincide: the product over s of f(g i) equals the product over s of f i, along atTop.
Русский
Если g инжективна и f равно единице вне образа g, то фильтры в atTop, получаемые через конечные произведения по f(g i) и по f i, совпадают.
LaTeX
$$$$\operatorname{map}\bigl(\lambda s. \prod_{i\in s} f(g(i))\bigr)\operatorname{atTop} = \operatorname{map}\bigl(\lambda s. \prod_{i\in s} f(i)\bigr)\operatorname{atTop}$$$$
Lean4
/-- 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`. -/
@[to_additive /-- 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`. -/
]
theorem map_atTop_finset_prod_le_of_prod_eq {f : α → M} {g : β → M}
(h_eq : ∀ u : Finset β, ∃ v : Finset α, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) :
(atTop.map fun s : Finset α => ∏ b ∈ s, f b) ≤ atTop.map fun s : Finset β => ∏ x ∈ s, g x := by
classical
refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_
let ⟨v, hv⟩ := h_eq b
refine ⟨v, trivial, ?_⟩
simpa [Finset.image_subset_iff] using hv
