frequently_bot — Mathlib

English

For any predicate p on α, there is no nonempty set in the bottom filter on which p holds for all elements of that set.

Русский

Для любого предиката p на α не существует множества S, принадлежащего нижнему фильтру, такого что p истина для всех элементов S.

LaTeX

$$$\\neg \\exists S\\, (S \\in \\bot \\wedge \\forall x\\in S,\\ p(x))$$$

Lean4

@[simp]
theorem frequently_bot {p : α → Prop} : ¬∃ᶠ x in ⊥, p x := by simp

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