mono — Mathlib

English

If p holds frequently with respect to f and p(x) implies q(x) for every x, then q holds frequently with respect to f.

Русский

Если p встречается часто по f и для каждого x выполняется p(x) ⇒ q(x), то q(x) встречается часто по f.

LaTeX

$$$ (\exists^\! x \in f, p(x)) \land (\forall x, p(x) \rightarrow q(x)) \rightarrow \exists^\! x \in f, q(x) $$$

Lean4

theorem mono {p q : α → Prop} {f : Filter α} (h : ∃ᶠ x in f, p x) (hpq : ∀ x, p x → q x) : ∃ᶠ x in f, q x :=
  h.mp (Eventually.of_forall hpq)

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