Frequently — Mathlib

English

The Frequent property f.Frequently p means that the set {x | ¬p x} does not belong to f; equivalently, p holds frequently along f.

Русский

Свойство Frequently(f, p) означает, что множество {x | ¬p(x)} не принадлежит f; эквивалентно, что p выполняется часто вдоль f.

LaTeX

$$$ \mathrm{Frequently}(p,f) \equiv \neg \forall^\infty x \in f, \neg p(x). $$$

Lean4

/-- `f.Frequently p` or `∃ᶠ x in f, p x` mean that `{x | ¬p x} ∉ f`. E.g., `∃ᶠ x in atTop, p x`
means that there exist arbitrarily large `x` for which `p` holds true. -/
protected def Frequently (p : α → Prop) (f : Filter α) : Prop :=
  ¬∀ᶠ x in f, ¬p x

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