support_comap — Mathlib

English

For a SummationFilter L on β and an embedding f: γ ↪ β, the support of the comapped filter equals the preimage of L.support under f.

Русский

Для сумматорного фильтра L на β и вложения f: γ ↪ β, опора фильтра, полученного комап, равна предобразу опоры L по f.

LaTeX

$$$(L.comap\ f).\\mathrm{support} = f^{-1}'(L.\\mathrm{support})$$$

Lean4

@[simp]
theorem support_comap (L : SummationFilter β) (f : γ ↪ β) : (L.comap f).support = f ⁻¹' L.support := by simp [support]

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