Equivalent alternative definitions concerning filters

Definition of a filter

Let E be a set.

Traditional definition of a filter on E: A collection \mathcal F of subsets of E is a filter on E iff \emptyset \notin E; and \forall A \in \mathcal F, \forall B \subseteq E, (B \supseteq A \implies B \in \mathcal F); and \forall A, B \in \mathcal F, A \cap B \in \mathcal F.

Alternative definition: A collection \mathcal F of subsets of E is a filter on E iff \emptyset \notin E; and \forall A, B \subseteq E, ((A, B) \in \mathcal F^2 \iff A \cap B \in \mathcal F).

The two definitions are equivalent.

Definition of the image of a filter

Let E and F be sets, \mathcal F a filter on E and f: E \to F.

Traditional definition: The filter on F image of \mathcal F by f is (f^{\rightarrow \rightarrow}(\mathcal F))^{\uparrow F}.

Alternative definition: The filter on F image of \mathcal F by f is \{\ B \subseteq F\ |\ f^\leftarrow(B) \in \mathcal F\ \}.

Again, the two definitions are equivalent.