LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)

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.

The upward closure of a filter base is the smallest filter containing it

Statement

Let $X$ be a set and let $B$ be a filter base on $X$ (Filter base and the filter it generates), with upward closure

$⟨ B ⟩ = {A \subseteq X : B \subseteq A for some B \in B} .$

Then:

$⟨ B ⟩$ is a filter on $X$ (Filter on a set);
$B \subseteq ⟨ B ⟩$ , and $⟨ B ⟩ \subseteq F$ for every filter $F$ on $X$ with $B \subseteq F$ , so $⟨ B ⟩$ is the smallest filter on $X$ containing $B$ ;
every filter $F$ on $X$ is itself a filter base, and it generates itself: $⟨ F ⟩ = F$ .

Facts & Assumptions

Given: A set $X$ , a filter base $B \subseteq P (X)$ , and $⟨ B ⟩$ as displayed in the statement.

[A1]

$B \neq \emptyset$ , $\emptyset \notin B$ , and for all $B_{1}, B_{2} \in B$ there is $B_{3} \in B$ with $B_{3} \subseteq B_{1} \cap B_{2}$ (Filter base and the filter it generates).

[L1]

A filter on $X$ is a family $F \subseteq P (X)$ with $X \in F$ , $\emptyset \notin F$ , $A \cap B \in F$ whenever $A, B \in F$ , and $B \in F$ whenever $A \in F$ and $A \subseteq B \subseteq X$ (Filter on a set).

[L2]

A filter base on $X$ is a nonempty family of subsets of $X$ that omits $\emptyset$ and is downward directed, the three conditions listed in [A1] (Filter base and the filter it generates).

Proof

technique · direct

1.1

Every member of $⟨ B ⟩$ is a subset of $X$ by definition, so $⟨ B ⟩ \subseteq P (X)$ ; and $X \in ⟨ B ⟩$ , since $B$ has a member $B$ and $B \subseteq X$ .

givenA1

1.2

$\emptyset \notin ⟨ B ⟩$ : if $B \subseteq \emptyset$ for some $B \in B$ then $B = \emptyset$ , and $\emptyset \notin B$ .

givenA1

1.3

$⟨ B ⟩$ is closed upward in $X$ : if $A \in ⟨ B ⟩$ , say $B \subseteq A$ with $B \in B$ , and $A \subseteq A^{'} \subseteq X$ , then $B \subseteq A^{'}$ , so $A^{'} \in ⟨ B ⟩$ .

given

1.4

$⟨ B ⟩$ is closed under pairwise intersection: given $A_{1}, A_{2} \in ⟨ B ⟩$ pick $B_{1}, B_{2} \in B$ with $B_{i} \subseteq A_{i}$ , and then $B_{3} \in B$ with $B_{3} \subseteq B_{1} \cap B_{2} \subseteq A_{1} \cap A_{2} \subseteq X$ , so $A_{1} \cap A_{2} \in ⟨ B ⟩$ .

givenA1

1.5

$B \subseteq ⟨ B ⟩$ , because $B \subseteq B$ and $B \subseteq X$ for every $B \in B$ .

given

1.6

If $F$ is a filter on $X$ with $B \subseteq F$ and $A \in ⟨ B ⟩$ , say $B \subseteq A \subseteq X$ with $B \in B \subseteq F$ , then upward closure of $F$ gives $A \in F$ ; hence $⟨ B ⟩ \subseteq F$ .

givenL1

1.7

Every filter $F$ on $X$ is a filter base: $X \in F$ gives $F \neq \emptyset$ , properness gives $\emptyset \notin F$ , and for $B_{1}, B_{2} \in F$ the member $B_{3} = B_{1} \cap B_{2}$ of $F$ satisfies $B_{3} \subseteq B_{1} \cap B_{2}$ .

L1L2

2.1

$⟨ B ⟩$ satisfies all four filter axioms, so it is a filter on $X$ .

step 1.1step 1.2step 1.3step 1.4L1

2.2

For a filter $F$ on $X$ , applying step 1.5 and step 1.6 to the filter base $F$ gives $F \subseteq ⟨ F ⟩$ and $⟨ F ⟩ \subseteq F$ , that is $⟨ F ⟩ = F$ .

step 1.7step 1.5step 1.6

3.1

So $⟨ B ⟩$ is a filter containing $B$ and contained in every filter that contains $B$ , hence the smallest such filter, and every filter is a filter base generating itself.

step 2.1step 2.2step 1.5step 1.6∎

Remarks

The only place directedness (B3) is used is step 1.4, the intersection axiom. Drop it and the upward closure of $B$ is still closed upward and still proper, but it need not be closed under intersection: on $X = {0, 1}$ the family $B = {{0}, {1}}$ has upward closure ${{0}, {1}, X}$ , which does not contain ${0} \cap {1} = \emptyset$ and is not a filter.
Part 3 is what licenses the phrase "the filter generated by" being applied to a filter: generation is idempotent, so nothing is gained by generating twice.
Smallest is meant in the inclusion order on $F i l t (X)$ and is a genuine least element of the set of filters containing $B$ , not merely a minimal one, since part 2 compares $⟨ B ⟩$ with every such filter. This is the opposite situation to Ultrafilter, where only maximality is available.

Depends on

Used by

Cited to discharge well-definedness by Filter base and the filter it generates.

Dependency tree · two levels

5 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

Filter (set theory) (Wikipedia) (standard reference, not scraped)
N. Bourbaki, General Topology: Chapters 1-4, Ch. I §6 (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)