Unbounded — Mathlib

English

An unbounded set is one that every element is dominated by some element of the set in the opposite direction; formally, ∀ a, ∃ b ∈ s with ¬ r b a.

Русский

Неограниченность множества означает, что для любого элемента существует элемент множества, не превосходящий его по отношению $r$; формально: ∀a ∃ b∈s, ¬ r b a.

LaTeX

$$∀ a, ∃ b ∈ s, ¬ r b a$$

Lean4

/-- An unbounded or cofinal set. -/
def Unbounded (r : α → α → Prop) (s : Set α) : Prop :=
  ∀ a, ∃ b ∈ s, ¬r b a

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