filter_mono — Mathlib

English

Let p be a property on α and f, g be filters on α with f ≤ g. If p holds frequently with respect to f, then p holds frequently with respect to g.

Русский

Пусть p — свойство на α, а f и g — фильтры на α так, что f ≤ g. Если p встречается часто по f, то она встречается часто и по g.

LaTeX

$$$ (\exists^\! x \in f, p(x)) \land (f \le g) \rightarrow \exists^\! x \in g, p(x) $$$

Lean4

theorem filter_mono {p : α → Prop} {f g : Filter α} (h : ∃ᶠ x in f, p x) (hle : f ≤ g) : ∃ᶠ x in g, p x :=
  mt (fun h' => h'.filter_mono hle) h

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