Definition (Filter). F⊆ℙ is called a filter if

  • (a) ∀⁡p,q∈F,∃⁡r∈F,r≤p,q
  • (b) ∀⁡p∈F,∀⁡q∈ℙ,q≥p⟹q∈F

If F only has property (a), we call it a filter base, and then

{p∈ℙ:∃⁡q∈F,q≤p}

is the filter generated from F.