English
If L is a SummationFilter on β with a well-defined support, and f is an embedding β → γ, then the mapped filter L.map f on γ also has a well-defined support.
Русский
Если L — сумматорный фильтр на β с определяемой опорой, и f: β ↪ γ — вложение, то образованный фильтр L.map f на γ также имеет определяемую опору.
LaTeX
$$$\\forall L\\,(\\text{HasSupport }L)\\;\\forall f:\\beta\\hookrightarrow\\gamma:\\;\\HasSupport(L.map f)$$$
Lean4
/-- If `L` has well-defined support, then so does its map along an embedding. -/
instance (L : SummationFilter β) [HasSupport L] (f : β ↪ γ) : HasSupport (L.map f) :=
by
constructor
by_cases h : L.NeBot
· simp only [map_filter, eventually_map, Finset.coe_map, image_subset_iff, support_map]
filter_upwards [L.eventually_le_support] with a using by grind
· have : L.filter = ⊥ := by contrapose! h; exact ⟨⟨h⟩⟩
simp [this]
