eventually_atTop_prod_self' — Mathlib

English

Let p be a predicate on α × α. With α directed by ≤, p holds eventually along atTop if and only if there exists a bound a such that p(k, l) holds for all k, l ≥ a.

Русский

Пусть p — предикат на пары из α × α. При направлении α по отношению ≤ свойство p выполняется вплоть до бесконечности слева и справа тогда, когда существует граница a, такая что для всех k, l ≥ a выполняется p(k, l).

LaTeX

$$$ (\forall^\infty x \in \mathrm{atTop},\ p(x)) \iff \exists a, \forall k \ge a, \forall l \ge a,\ p(k,l) $$$

Lean4

theorem eventually_atTop_prod_self' [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {p : α × α → Prop} :
    (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l) := by
  simp only [eventually_atTop_prod_self, forall_cond_comm]

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