support_map — Mathlib

English

The support of the mapped summation filter equals the image of the original support under the embedding.

Русский

Поддержка отображенного фильтра суммирования равна образу поддержки исходного фильтра через вложение.

LaTeX

$$$$\\mathrm{support}(L\\map f) = f'' \\mathrm{support}(L).$$$$

Lean4

@[simp]
theorem support_map (L : SummationFilter β) [L.NeBot] (f : β ↪ γ) : (L.map f).support = f '' L.support :=
  by
  ext c
  rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc
  · simp [support]
  ·
    exact
      ⟨fun hc' ↦
        have := hc'.exists;
        by grind,
        by grind⟩

Похожие утверждения