Filter bases
A filter basis B : filter_basis α on a type α is a nonempty collection of sets of α
such that the intersection of two elements of this collection contains some element of
the collection. Compared to filters, filter bases do not require that any set containing
an element of B belongs to B.
A filter basis B can be used to construct B.filter : filter α such that a set belongs
to B.filter if and only if it contains an element of B.
Given an indexing type ι, a predicate p : ι → Prop, and a map s : ι → set α,
the proposition h : filter.is_basis p s makes sure the range of s bounded by p
(ie. s '' set_of p) defines a filter basis h.filter_basis.
If one already has a filter l on α, filter.has_basis l p s (where p : ι → Prop
and s : ι → set α as above) means that a set belongs to l if and
only if it contains some s i with p i. It implies h : filter.is_basis p s, and
l = h.filter_basis.filter. The point of this definition is that checking statements
involving elements of l often reduces to checking them on the basis elements.
This file also introduces more restricted classes of bases, involving monotonicity or
countability. In particular, for l : filter α, l.is_countably_generated means
there is a countable set of sets which generates s. This is reformulated in term of bases,
and consequences are derived.
Main statements
has_basis.mem_iff,has_basis.mem_of_superset,has_basis.mem_of_mem: restatet ∈ fin terms of a basis;basis_sets: all sets of a filter form a basis;has_basis.inf,has_basis.inf_principal,has_basis.prod,has_basis.prod_self,has_basis.map,has_basis.comap: combinators to construct filters ofl ⊓ l',l ⊓ 𝓟 t,l ×ᶠ l',l ×ᶠ l,l.map f,l.comap frespectively;has_basis.le_iff,has_basis.ge_iff, has_basis.le_basis_iff: restatel ≤ l'` in terms of bases.has_basis.tendsto_right_iff,has_basis.tendsto_left_iff,has_basis.tendsto_iff: restatetendsto f l l'in terms of bases.is_countably_generated_iff_exists_antimono_basis: proves a filter is countably generated if and only if it admis a basis parametrized by a decreasing sequence of sets indexed byℕ.tendsto_iff_seq_tendsto: an abstract version of "sequentially continuous implies continuous".
Implementation notes
As with Union/bUnion/sUnion, there are three different approaches to filter bases:
has_basis l s,s : set (set α);has_basis l s,s : ι → set α;has_basis l p s,p : ι → Prop,s : ι → set α.
We use the latter one because, e.g., 𝓝 x in an emetric_space or in a metric_space has a basis
of this form. The other two can be emulated using s = id or p = λ _, true.
With this approach sometimes one needs to simp the statement provided by the has_basis
machinery, e.g., simp only [exists_prop, true_and] or simp only [forall_const] can help
with the case p = λ _, true.
- sets : set (set α)
- nonempty : c.sets.nonempty
- inter_sets : ∀ {x y : set α}, x ∈ c.sets → y ∈ c.sets → (∃ (z : set α) (H : z ∈ c.sets), z ⊆ x ∩ y)
A filter basis B on a type α is a nonempty collection of sets of α
such that the intersection of two elements of this collection contains some element
of the collection.
Equations
- _ = _
If B is a filter basis on α, and U a subset of α then we can write U ∈ B as on paper.
Equations
- filter_basis.has_mem = {mem := λ (U : set α) (B : filter_basis α), U ∈ B.sets}
Equations
- filter_basis.inhabited = {default := {sets := set.range set.Ici, nonempty := filter_basis.inhabited._proof_1, inter_sets := filter_basis.inhabited._proof_2}}
Constructs a filter basis from an indexed family of sets satisfying is_basis.
Equations
- h.filter_basis = {sets := s '' set_of p, nonempty := _, inter_sets := _}
The filter associated to a filter basis.
Constructs a filter from an indexed family of sets satisfying is_basis.
Equations
- h.filter = h.filter_basis.filter
We say that a filter l has a basis s : ι → set α bounded by p : ι → Prop,
if t ∈ l if and only if t includes s i for some i such that p i.
The smallest filter basis containing a given collection of sets.
Equations
- filter.filter_basis.of_sets s = {sets := set.sInter '' {t : set (set α) | t.finite ∧ t ⊆ s}, nonempty := _, inter_sets := _}
If {s i | p i} is a basis of a filter l and each s i includes s j such that
p j ∧ q j, then {s j | p j ∧ q j} is a basis of l.
If {s i | p i} is a basis of a filter l and V ∈ l, then {s i | p i ∧ s i ⊆ V}
is a basis of l.
If s : ι → set α is an indexed family of sets, then finite intersections of s i form a basis
of ⨅ i, 𝓟 (s i).
- to_is_basis : filter.is_basis p s
- decreasing : ∀ {i j : ι}, p i → p j → i ≤ j → s j ⊆ s i
- mono : monotone p
is_antimono_basis p s means the image of s bounded by p is a filter basis
such that s is decreasing and p is increasing, ie i ≤ j → p i → p j.
- to_has_basis : l.has_basis p s
- decreasing : ∀ {i j : ι}, p i → p j → i ≤ j → s j ⊆ s i
- mono : monotone p
We say that a filter l has a antimono basis s : ι → set α bounded by p : ι → Prop,
if t ∈ l if and only if t includes s i for some i such that p i,
and s is decreasing and p is increasing, ie i ≤ j → p i → p j.
is_countably_generated f means f = generate s for some countable s.
Equations
- f.is_countably_generated = ∃ (s : set (set α)), s.countable ∧ f = filter.generate s
- to_is_basis : filter.is_basis p s
- countable : (set_of p).countable
is_countable_basis p s means the image of s bounded by p is a countable filter basis.
We say that a filter l has a countable basis s : ι → set α bounded by p : ι → Prop,
if t ∈ l if and only if t includes s i for some i such that p i, and the set
defined by p is countable.
- to_filter_basis : filter_basis α
- countable : c.to_filter_basis.sets.countable
A countable filter basis B on a type α is a nonempty countable collection of sets of α
such that the intersection of two elements of this collection contains some element
of the collection.
Equations
- filter.nat.inhabited_countable_filter_basis = {default := {to_filter_basis := {sets := (inhabited.default (filter_basis ℕ)).sets, nonempty := filter.nat.inhabited_countable_filter_basis._proof_1, inter_sets := filter.nat.inhabited_countable_filter_basis._proof_2}, countable := filter.nat.inhabited_countable_filter_basis._proof_3}}
A set generating a countably generated filter.
Equations
A countable filter basis for a countably generated filter.
Equations
- h.countable_filter_basis = {to_filter_basis := {sets := (filter.filter_basis.of_sets h.generating_set).sets, nonempty := _, inter_sets := _}, countable := _}