frequently_atBot — Mathlib

English

Let p be a property on α with directed order and nonempty domain. The predicate p holds frequently along atBot if and only if for every a, there exists b ≤ a with p(b).

Русский

Пусть p — свойство на α с направленным порядком и непустым множеством значений. Свойство p встречается часто в направлении atBot тогда и только если для каждого a существует b ≤ a such that p(b).

LaTeX

$$$(\exists\!\text{freq} x\ in\ atBot, p x) \leftrightarrow \forall a, \exists b \le a, p b$$$

Lean4

theorem frequently_atBot : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b ≤ a, p b :=
  frequently_atTop (α := αᵒᵈ)

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