Filter Contains Greatest Element
Jump to navigation
Jump to search
This article needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code. |
Theorem
Let $\struct{S, \preceq}$ be an ordered set with greatest element $\top$.
Let $\FF$ be a filter in $\struct{S, \preceq}$.
Then:
- $\top \in \FF$
Proof
- $\exists x \in \FF$
By definition of greatest element: $x \preceq \top$
- $\top \in \FF$
$\blacksquare$