isBounded_top — Mathlib

English

IsBounded r ⊤ is equivalent to the existence of t with ∀ x, r(x,t); the top filter is bounded precisely when such a t exists.

Русский

IsBounded r ⊤ эквивалентно существованию t с ∀ x, r(x,t); верхний фильтр ограничен точно тогда, когда существует такой t.

LaTeX

$$$$ \text{IsBounded } r \; \top \ \Longleftrightarrow \ \exists t, \forall x, r(x,t) $$$$

Lean4

theorem isBounded_top : IsBounded r ⊤ ↔ ∃ t, ∀ x, r x t := by simp [IsBounded]

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