frequently_atBot' — Mathlib

English

Under NoMinOrder, the frequency atBot of p is equivalent to p being true below every a in α with a witness b < a.

Русский

При NoMinOrder α частотность atBot совпадает с утверждением: для каждого a существует b < a, такое что p(b).

LaTeX

$$$[NoMinOrder\ α]\ (\exists\!\text{freq} x\ in\ atBot, p x) \leftrightarrow \forall a, \exists b < a, p b$$$

Lean4

theorem frequently_atBot' [NoMinOrder α] : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b < a, p b :=
  frequently_atTop' (α := αᵒᵈ)

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