English
If g is injective and hf is 1 outside range g, then the two atTop pushforwards of finite set products coincide: the equality holds for all finite sets via g and directly.
Русский
Если g инъективна и hf ≡ 1 за пределами образа g, тогда равенство фильтров на atTop для двух отображений произведений по g и по исходному f выполняется.
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 `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
to a commutative monoid. Suppose that `f x = 1` outside of the range of `g`. Then the filters
`atTop.map (fun s ↦ ∏ i ∈ s, f (g i))` and `atTop.map (fun s ↦ ∏ i ∈ s, f i)` coincide.
The additive version of this lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
the same assumptions. -/
@[to_additive]
theorem map_atTop_finset_prod_eq {g : α → β} (hg : Function.Injective g) {f : β → M}
(hf : ∀ x, x ∉ Set.range g → f x = 1) : map (fun s => ∏ i ∈ s, f (g i)) atTop = map (fun s => ∏ i ∈ s, f i) atTop :=
by
haveI := Classical.decEq β
apply le_antisymm <;> refine map_atTop_finset_prod_le_of_prod_eq fun s => ?_
· refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
rw [← Finset.prod_image hg.injOn]
refine (prod_subset subset_union_left ?_).symm
simp only [Finset.mem_union, Finset.mem_image]
refine fun y hy hyt => hf y (mt ?_ hyt)
rintro ⟨x, rfl⟩
exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩
· refine ⟨s.image g, fun t ht => ?_⟩
simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]
exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩
