Topological filters in Isabelle

I'm studying topological filters in Filter.thy


theory Filter
imports Set_Interval Lifting_Set
begin

subsection ‹Filters›

text ‹
  This definition also allows non-proper filters.
›

locale is_filter =
  fixes F :: "('a ⇒ bool) ⇒ bool"
  assumes True: "F (λx. True)"
  assumes conj: "F (λx. P x) ⟹ F (λx. Q x) ⟹ F (λx. P x ∧ Q x)"
  assumes mono: "∀x. P x ⟶ Q x ⟹ F (λx. P x) ⟹ F (λx. Q x)"

typedef 'a filter = "{F :: ('a ⇒ bool) ⇒ bool. is_filter F}"
proof
  show "(λx. True) ∈ ?filter" by (auto intro: is_filter.intro)
qed

I don't get this definition. It's quite convoluted so I'll simplify it first

The expression F (λx. P x) could be simplified to F P (using eta reduction of lambda calculus). The predicate 'a ⇒ bool is really just a set 'a set. Similarly ('a ⇒ bool) ⇒ bool should be 'a set set. Then we could rewrite the axioms as

assumes conj: "P ∈ F ∧ Q ∈ F ⟹ Q ∩ P ∈ F"
assumes mono: "P ⊆ Q ∧ P ∈ F ⟹ Q ∈ F"

Now my question is about the True axiom. It is equivalent to

assumes True: "UNIV ∈ F"

This does not match with the definitions of filters that I ever saw. The axiom should be instead

assumes True: "{} ∉ F"  (* the name True is not very fitting anymore *)

The statement UNIV ∈ F is unnecessary because it follows from axiom mono.

So what's up with this definition that Isabelle provides?

Solution

The link provided by Javier Diaz has lots of explanations.

Turns out this is a definition of improper filter. The axiom True is necessary and does not follow from mono. If this axiom was missing then F could be defined as

F P = False

or in set-theory notation, F could be an empty set and mono and conj would then be satisfied vacuously.