inf_neBot_iff_frequently_right — Mathlib

English

For filters f and g on α, NeBot (f ⊓ g) is equivalent to: for every predicate p on α, if p holds frequently in g, then p holds frequently in f.

Русский

Для фильтров f и g на α неботовская связка f ⊓ g эквивалентна тому, что для каждого p : α → Prop, если p часто встречается в g, тогда часто встречается в f.

LaTeX

$$$ \mathrm{NeBot}(f \cap g) \iff \forall p: \alpha \to \mathrm{Prop}, (\forall^\infty x \text{ in } g, p x) \to (\exists^\infty x \text{ in } f, p x) $$$

Lean4

theorem inf_neBot_iff_frequently_right {f g : Filter α} :
    NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in g, p x) → ∃ᶠ x in f, p x :=
  by
  rw [inf_comm]
  exact inf_neBot_iff_frequently_left

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