eventually_forall_le_atBot — Mathlib

English

Dual statement to AtTopGe: eventually for all smaller elements is equivalent to pointwise eventual truth.

Русский

Двойственное утверждение к AtTopGe: рано или поздно верно для всех меньших элементов эквивалентно поэлементной верности.

LaTeX

$$$[\text{Preorder } \alpha] \\ (\forall^\infty x \in \operatorname{atBot}, \forall y, y \le x \Rightarrow p(y)) \iff (\forall^\infty x \in \operatorname{atBot}, p(x))$$$

Lean4

theorem eventually_forall_le_atBot [Preorder α] {p : α → Prop} :
    (∀ᶠ x in atBot, ∀ y, y ≤ x → p y) ↔ ∀ᶠ x in atBot, p x :=
  eventually_forall_ge_atTop (α := αᵒᵈ)

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