mono_filter — Mathlib

English

If a function is Multipliable with respect to a larger filter L2 and L1's filter is contained in L2's, then the same function is Multipliable with respect to L1.

Русский

Если f суммируемо по L2, и фильтр L1 подпадает под L2, то f суммируемо по L1.

LaTeX

$$$ Multipliable f L_2 \rightarrow (L_1.filter \le L_2.filter) \rightarrow Multipliable f L_1 $$$

Lean4

@[to_additive]
theorem mono_filter {f : β → α} {L₁ L₂ : SummationFilter β} (hf : Multipliable f L₂) (h : L₁.filter ≤ L₂.filter) :
    Multipliable f L₁ :=
  match hf with
  | ⟨a, ha⟩ => ⟨a, ha.mono_left h⟩

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