isBounded_bot — Mathlib

English

IsBounded r ⊥ is equivalent to Nonempty α; a bottom filter is bounded exactly when the base type is nonempty.

Русский

IsBounded r ⊥ эквивалентно Nonempty α; нижний фильтр ограничен тогда и только тогда, когда множество оснований непусто.

LaTeX

$$$$ \text{IsBounded } r \; \bot \ \longleftrightarrow \ \text{Nonempty } \alpha $$$$

Lean4

theorem isBounded_bot : IsBounded r ⊥ ↔ Nonempty α := by simp [IsBounded, exists_true_iff_nonempty]

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