inf_neBot_iff_frequently_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inf_neBot_iff_frequently_left {f g : Filter α} :
    NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x := by
  simp only [inf_neBot_iff, frequently_iff, and_comm]; rfl

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