LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A family lies in a filter exactly when it has the finite intersection property

Statement

Let $X$ be a set and $A \subseteq P (X)$ . Write

$A^{\cap} : = {⋂_{i \in n} s (i) : n \in N, s : n \to A}$

for the family of intersections of finite lists in $A$ (Finite intersection property), which contains $X$ as the empty intersection. Then:

$A^{\cap}$ is closed under pairwise intersection and contains $A \cup {X}$ ;
if $A$ has the finite intersection property, then $A^{\cap}$ is a filter base on $X$ (Filter base and the filter it generates) and $⟨ A^{\cap} ⟩$ is the smallest filter on $X$ containing $A$ (Filter on a set, The upward closure of a filter base is the smallest filter containing it);
conversely, if $A \subseteq F$ for some filter $F$ on $X$ , then $A$ has the finite intersection property.

Consequently a family of subsets of $X$ is contained in some filter on $X$ if and only if it has the finite intersection property.

Facts & Assumptions

Given: A set $X$ , a family $A \subseteq P (X)$ , and $A^{\cap}$ as displayed in the statement. Parts 2 and 3 assume, respectively, that $A$ has the finite intersection property and that $A$ is contained in a filter on $X$ .

[A1]

$A$ has the finite intersection property when $⋂_{i \in n} s (i) \neq \emptyset$ for every $n \in N$ and every $s : n \to A$ , the case $n = 0$ reading $X \neq \emptyset$ (Finite intersection property).

[L1]

A filter on $X$ contains $X$ , omits $\emptyset$ , is closed under pairwise intersection, and is closed upward in $X$ (Filter on a set).

[L2]

A filter base on $X$ is nonempty, omits $\emptyset$ , and is downward directed; its upward closure is the smallest filter on $X$ containing it (Filter base and the filter it generates, The upward closure of a filter base is the smallest filter containing it).

[L3]

In the von Neumann encoding $σ (n) = n \cup {n}$ and $n \notin n$ , so, $A$ being nonempty, a function $u : n \to A$ extends to a function $u^{'} : σ (n) \to A$ by prescribing $u^{'} (n)$ to be any member of $A$ (The natural numbers $N$ (von Neumann), Every natural number is a transitive set and is not a member of itself).

[L4]

Induction on $N$ : a property holding at $0$ and passing from $n$ to $σ (n)$ holds for every natural number (The principle of mathematical induction).

Proof

technique · direct

1.1

Every member of $A^{\cap}$ is a subset of $X$ , and $X \in A^{\cap}$ as the intersection of the empty list, so $A^{\cap} \neq \emptyset$ .

givenA1

1.2

$A \subseteq A^{\cap}$ : for $A \in A$ the list $s : 1 \to A$ with $s (0) = A$ has $⋂_{i \in 1} s (i) = A$ , since $1 = σ (0) = {0}$ .

givenL3

1.3

Adjoining one member keeps the family: if $B = ⋂_{k \in p} u (k) \in A^{\cap}$ and $A \in A$ , then extending $u$ to $u^{'} : σ (p) \to A$ with $u^{'} (p) = A$ gives $⋂_{k \in σ (p)} u^{'} (k) = B \cap A$ , so $B \cap A \in A^{\cap}$ .

givenL3

1.4

Splitting off the last entry: for $t : σ (n) \to A$ one has $⋂_{j \in σ (n)} t (j) = (⋂_{j \in n} t (j)) \cap t (n)$ , since $σ (n) = n \cup {n}$ .

givenL3

1.5

If $A$ has the finite intersection property then no member of $A^{\cap}$ is empty, that is $\emptyset \notin A^{\cap}$ .

A1given

2.1

$A^{\cap}$ is closed under pairwise intersection, by induction on the length $n$ of the second list: for $n = 0$ the second intersection is $X$ and $B \cap X = B \in A^{\cap}$ ; and if the claim holds for all lists of length $n$ , then for $t : σ (n) \to A$ the set $B \cap ⋂_{j \in σ (n)} t (j) = (B \cap ⋂_{j \in n} t (j)) \cap t (n)$ lies in $A^{\cap}$ by the case $n$ followed by step 1.3.

step 1.3step 1.4L4

2.2

Every filter $F$ on $X$ with $A \subseteq F$ satisfies $A^{\cap} \subseteq F$ , by induction on the length $n$ of the list: the empty intersection is $X \in F$ , and $⋂_{j \in σ (n)} t (j) = (⋂_{j \in n} t (j)) \cap t (n)$ is an intersection of two members of $F$ .

step 1.4L1L4

3.1

Under the finite intersection property, $A^{\cap}$ is a filter base on $X$ : it is nonempty by step 1.1, omits $\emptyset$ by step 1.5, and is downward directed because $B_{1} \cap B_{2}$ itself lies in $A^{\cap}$ .

step 1.1step 1.5step 2.1L2

3.2

Conversely, if $A \subseteq F$ with $F$ a filter on $X$ , then $A^{\cap} \subseteq F$ and $\emptyset \notin F$ , so no intersection of a finite list in $A$ is empty: $A$ has the finite intersection property.

step 2.2L1A1

4.1

Under the finite intersection property, $⟨ A^{\cap} ⟩$ is the smallest filter on $X$ containing $A$ : it is a filter containing $A^{\cap} \supseteq A$ , and any filter containing $A$ contains $A^{\cap}$ and hence its upward closure.

step 3.1step 2.2step 1.2L2

5.1

So $A^{\cap}$ contains $A \cup {X}$ and is closed under pairwise intersection, and $A$ is contained in some filter on $X$ if and only if it has the finite intersection property, in which case the smallest such filter is $⟨ A^{\cap} ⟩$ .

step 1.1step 1.2step 2.1step 4.1step 3.2∎

Remarks

Where the hypothesis bites. Part 1 is unconditional: finite lists can always be extended one entry at a time. Only properness, $\emptyset \notin A^{\cap}$ , needs the finite intersection property, and it is exactly that property restated. So the content of the lemma is bookkeeping in one direction and a definition unfolded in the other, which is why the finite intersection property is the right hypothesis rather than a convenient one.
The proof uses induction only to move along the length of a list. No theory of finite sets is needed, because a finite list is a function out of a natural number and a natural number is its own set of predecessors (The natural numbers $N$ (von Neumann)).
The empty list matters twice: it puts $X$ into $A^{\cap}$ , which is what makes $A^{\cap}$ nonempty even when $A$ is empty, and it is the base case of both inductions. With the $n \geq 1$ reading of the finite intersection property one would have to add $A \neq \emptyset$ as a hypothesis to part 2.
The generated filter $⟨ A^{\cap} ⟩$ is the filter usually written $⟨ A ⟩$ and called the filter generated by $A$ . It is only defined when $A$ has the finite intersection property, which is why this library names the base explicitly.

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Finite intersection property (Wikipedia) (standard reference, not scraped)
Filter (set theory) (Wikipedia) (standard reference, not scraped)
N. Strickland, Notes on Ultrafilters (standard reference, not scraped)
B. Kaya, Ultrafilters and How to Use Them (standard reference, not scraped)