namespace http://mathhub.info/MitM/core/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚

theory UpDownSet : base:?Logic = 
   include ?POSet ❙
   upset : {P : poset} (set (P.universe)) ⟶ bool ❘ = [P,F] ∀[x] ∀[y] x ∈ F ∧ (P.ord) x y ⇒ y ∈ F ❘ # upset 2❙
   downset : {P : poset} (set (P.universe)) ⟶ bool ❘ = [P,F] ∀[x] ∀[y] x ∈ F ∧ (P.ord) y x ⇒ y ∈ F ❘ # downset 2❙
❚  

theory filter : base:?Logic = 
  include ?POSet ❙
  include ?UpDownSet ❙
  include ?Relations ❙
  include ?LeastMost ❙
  include ?DirectedSet❙
  prop_isFilter : {P : poset} (set (P.universe)) ⟶ bool ❘ = [P,F] upset F ∧ (P.prop_directedSubset) F ❘ # isFilter 2❙
  prop_isProperFilter : {P : poset}  (set (P.universe)) ⟶ bool ❘ = [P,F] isFilter F ∧ ¬ F ≐ fullset (P.universe) ❙
  prop_isUltrafilter : {P : poset} (set (P.universe)) ⟶ bool ❘ = [P,F] isGreatest F ([x] isFilter x) ([x,y] subset (P.universe) x y) ❙
❚