filter_mono — Mathlib

English

If f1 ≤ f2 then every predicate that holds eventually in f2 also holds eventually in f1.

Русский

Если f1 ≤ f2, то для каждого p, выполняющегося eventually в f2, выполняется и в f1.

LaTeX

$$$f_1 \\le f_2 \\Rightarrow (\\forall p, \\text{Eventually}(p, f_2) \\Rightarrow \\text{Eventually}(p, f_1))$$$

Lean4

theorem filter_mono {f₁ f₂ : Filter α} (h : f₁ ≤ f₂) {p : α → Prop} (hp : ∀ᶠ x in f₂, p x) : ∀ᶠ x in f₁, p x :=
  h hp

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