RestrictedProduct.nhds_zero_eq_map_ofPre statement

Stream: mathlib4

[Matthew Jasper]

Is the conclusion of this lemma supposed to be 𝓝 0 = .map (inclusion R (fun i ↦ B i) hT) (𝓝 0)? The current version is no more useful than nhds_eq_map_inclusion. Should I make a PR to change this or make a new lemma?