eventually_atBot_prod_self — Mathlib

English

In a directed preorder with Nonempty domain, an eventually true property on pairs is equivalent to the existence of a common bound a such that p(k,l) holds for all k,l ≤ a.

Русский

В направленном порядке с непустым множеством, свойство p на паре эквивалентно существованию верхней границы a, такой что p(k,l) выполняется для всех k,l ≤ a.

LaTeX

$$$(\\forall\\text{ᶠ } x \\in \\operatorname{atBot}, p x) \\iff \\exists a, \\forall k, l, k \\le a \\rightarrow l \\le a \\rightarrow p (k, l)$$$

Lean4

theorem eventually_atBot_prod_self [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {p : α × α → Prop} :
    (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k l, k ≤ a → l ≤ a → p (k, l) := by
  simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

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