eventually_atBot — Mathlib

English

Let p be a property on a directed preorder α with [Nonempty α]. The property p holds eventually near the bottom if and only if there exists a threshold a such that p holds for every b with b ≤ a.

Русский

Пусть p — свойство на частично упорядоченном направленном множестве α с непустым элементом. Свойство p выполняется у нижнего конца «насколько можно», если и только если существует порог a, такой что для всех b, удовлетворяющих b ≤ a, выполняется p(b).

LaTeX

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

Lean4

@[simp]
theorem eventually_atBot : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b :=
  mem_atBot_sets

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