Filter bases

A filter basis B : FilterBasis α 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→ Prop, and a map s : ι → set α→ set α, the proposition h : Filter.IsBasis 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.HasBasis l p s (where p : ι → Prop→ Prop and s : ι → set α→ 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.IsBasis p s, and l = h.filterBasis.filter. The point of this definition is that checking statements involving elements of l often reduces to checking them on the basis elements.

We define a function HasBasis.index (h : Filter.HasBasis l p s) (t) (ht : t ∈ l)∈ l) that returns some index i such that p i and s i ⊆ t⊆ t. This function can be useful to avoid manual destruction of h.mem_iff.mpr ht using cases or let.

This file also introduces more restricted classes of bases, involving monotonicity or countability. In particular, for l : Filter α, l.IsCountablyGenerated means there is a countable set of sets which generates s. This is reformulated in term of bases, and consequences are derived.

Main statements

• Filter.HasBasis.mem_iff, HasBasis.mem_of_superset, HasBasis.mem_of_mem : restate t ∈ f∈ f in terms of a basis;

• Filter.basis_sets : all sets of a filter form a basis;

• Filter.HasBasis.inf, Filter.HasBasis.inf_principal, Filter.HasBasis.prod, Filter.HasBasis.prod_self, Filter.HasBasis.map, Filter.HasBasis.comap : combinators to construct filters of l ⊓ l'⊓ l', l ⊓ 𝓟 t⊓ 𝓟 t, l ×ᶠ l'×ᶠ l', l ×ᶠ l×ᶠ l, l.map f, l.comap f respectively;

• Filter.HasBasis.le_iff, Filter.HasBasis.ge_iff, Filter.HasBasis.le_basis_iff : restate l ≤ l'≤ l' in terms of bases.

• Filter.HasBasis.tendsto_right_iff, Filter.HasBasis.tendsto_left_iff, Filter.HasBasis.tendsto_iff : restate tendsto f l l' in terms of bases.

• is_countably_generated_iff_exists_antitone_basis : proves a filter is countably generated if and only if it admits 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 Set.unionᵢ/bunionᵢ/Set.unionₛ, there are three different approaches to filter bases:

• Filter.HasBasis l s, s : set (set α);
• Filter.HasBasis l s, s : ι → set α→ set α;
• Filter.HasBasis l p s, p : ι → Prop→ Prop, s : ι → set α→ 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 Filter.HasBasis machinery, e.g., simp only [true_and] or simp only [forall_const] can help with the case p = λ _, true.

ink

structure FilterBasis (α : Type u_1) : Type u_1

• Sets of a filter basis.

  sets : Set (Set α)

• The set of filter basis sets is nonempty.

  nonempty : Set.Nonempty sets

• The set of filter basis sets is directed downwards.

  inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z, z ∈ 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.

ink

instance FilterBasis.nonempty_sets {α : Type u_1} (B : FilterBasis α) : Nonempty ↑B.sets

Equations

• @FilterBasis.nonempty_sets = @FilterBasis.nonempty_sets.proof_1

ink

instance instMembershipSetFilterBasis {α : Type u_1} : Membership (Set α) (FilterBasis α)

If B is a filter basis on α, and U a subset of α then we can write U ∈ B∈ B as on paper.

Equations

• instMembershipSetFilterBasis = { mem := fun U B => U ∈ B.sets }

ink

@[simp]

theorem FilterBasis.mem_sets {α : Type u_1} {s : Set α} {B : FilterBasis α} : s ∈ B.sets ↔ s ∈ B

ink

instance instInhabitedFilterBasisNat : Inhabited (FilterBasis ℕ)

Equations

• instInhabitedFilterBasisNat = { default := { sets := Set.range Set.Ici, nonempty := instInhabitedFilterBasisNat.proof_1, inter_sets := @instInhabitedFilterBasisNat.proof_2 } }

ink

def Filter.asBasis {α : Type u_1} (f : Filter α) : FilterBasis α

View a filter as a filter basis.

Equations

• Filter.asBasis f = { sets := f.sets, nonempty := (_ : ∃ x, x ∈ f.sets), inter_sets := (_ : ∀ {x y : Set α}, x ∈ f.sets → y ∈ f.sets → ∃ z, z ∈ f.sets ∧ z ⊆ x ∩ y) }

ink

structure Filter.IsBasis {α : Type u_1} {ι : Sort u_2} (p : ι → Prop) (s : ι → Set α) : Prop

• There exists at least one i that satisfies p.

  nonempty : ∃ i, p i

• s is directed downwards on i such that p i.

  inter : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j

is_basis p s means the image of s bounded by p is a filter basis.

ink

def Filter.IsBasis.filterBasis {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : FilterBasis α

Constructs a filter basis from an indexed family of sets satisfying IsBasis.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Filter.IsBasis.mem_filterBasis_iff {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α} : U ∈ Filter.IsBasis.filterBasis h ↔ ∃ i, p i ∧ s i = U

ink

def FilterBasis.filter {α : Type u_1} (B : FilterBasis α) : Filter α

The filter associated to a filter basis.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem FilterBasis.mem_filter_iff {α : Type u_1} (B : FilterBasis α) {U : Set α} : U ∈ FilterBasis.filter B ↔ ∃ s, s ∈ B ∧ s ⊆ U

ink

theorem FilterBasis.mem_filter_of_mem {α : Type u_1} (B : FilterBasis α) {U : Set α} : U ∈ B → U ∈ FilterBasis.filter B

ink

theorem FilterBasis.eq_infᵢ_principal {α : Type u_1} (B : FilterBasis α) : FilterBasis.filter B = ⨅ s, Filter.principal ↑s

ink

theorem FilterBasis.generate {α : Type u_1} (B : FilterBasis α) : Filter.generate B.sets = FilterBasis.filter B

ink

def Filter.IsBasis.filter {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter α

Constructs a filter from an indexed family of sets satisfying IsBasis.

Equations

• Filter.IsBasis.filter h = FilterBasis.filter (Filter.IsBasis.filterBasis h)

ink

theorem Filter.IsBasis.mem_filter_iff {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α} : U ∈ Filter.IsBasis.filter h ↔ ∃ i, p i ∧ s i ⊆ U

ink

theorem Filter.IsBasis.filter_eq_generate {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter.IsBasis.filter h = Filter.generate { U | ∃ i, p i ∧ s i = U }

ink

structure Filter.HasBasis {α : Type u_1} {ι : Sort u_2} (l : Filter α) (p : ι → Prop) (s : ι → Set α) : Prop

• A set t belongs to a filter l iff it includes an element of the basis.

  mem_iff' : ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

We say that a filter l has a basis s : ι → set α→ set α bounded by p : ι → Prop→ Prop, if t ∈ l∈ l if and only if t includes s i for some i such that p i.

ink

theorem Filter.hasBasis_generate {α : Type u_1} (s : Set (Set α)) : Filter.HasBasis (Filter.generate s) (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t

ink

def Filter.FilterBasis.ofSets {α : Type u_1} (s : Set (Set α)) : FilterBasis α

The smallest filter basis containing a given collection of sets.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Filter.FilterBasis.ofSets_sets {α : Type u_1} (s : Set (Set α)) : (Filter.FilterBasis.ofSets s).sets = Set.interₛ '' { t | Set.Finite t ∧ t ⊆ s }

ink

theorem Filter.HasBasis.mem_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (hl : Filter.HasBasis l p s) : t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

Definition of HasBasis unfolded with implicit set argument.

ink

theorem Filter.HasBasis.eq_of_same_basis {α : Type u_1} {ι : Sort u_2} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p s) : l = l'

ink

theorem Filter.hasBasis_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} : Filter.HasBasis l p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

ink

theorem Filter.HasBasis.ex_mem {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : ∃ i, p i

ink

theorem Filter.HasBasis.nonempty {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Nonempty ι

ink

theorem Filter.IsBasis.hasBasis {α : Type u_1} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter.HasBasis (Filter.IsBasis.filter h) p s

ink

theorem Filter.HasBasis.mem_of_superset {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} {i : ι} (hl : Filter.HasBasis l p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l

ink

theorem Filter.HasBasis.mem_of_mem {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {i : ι} (hl : Filter.HasBasis l p s) (hi : p i) : s i ∈ l

ink

noncomputable def Filter.HasBasis.index {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) (t : Set α) (ht : t ∈ l) : { i // p i }

Index of a basis set such that s i ⊆ t⊆ t as an element of subtype p.

Equations

• Filter.HasBasis.index h t ht = { val := Exists.choose (_ : ∃ i, p i ∧ s i ⊆ t), property := Filter.HasBasis.index.proof_2 h t ht }

ink

theorem Filter.HasBasis.property_index {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : p ↑(Filter.HasBasis.index h t ht)

ink

theorem Filter.HasBasis.set_index_mem {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : s ↑(Filter.HasBasis.index h t ht) ∈ l

ink

theorem Filter.HasBasis.set_index_subset {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : s ↑(Filter.HasBasis.index h t ht) ⊆ t

ink

theorem Filter.HasBasis.isBasis {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.IsBasis p s

ink

theorem Filter.HasBasis.filter_eq {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.IsBasis.filter (_ : Filter.IsBasis p s) = l

ink

theorem Filter.HasBasis.eq_generate {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : l = Filter.generate { U | ∃ i, p i ∧ s i = U }

ink

theorem Filter.generate_eq_generate_inter {α : Type u_1} (s : Set (Set α)) : Filter.generate s = Filter.generate (Set.interₛ '' { t | Set.Finite t ∧ t ⊆ s })

ink

theorem Filter.ofSets_filter_eq_generate {α : Type u_1} (s : Set (Set α)) : FilterBasis.filter (Filter.FilterBasis.ofSets s) = Filter.generate s

ink

theorem FilterBasis.hasBasis {α : Type u_1} (B : FilterBasis α) : Filter.HasBasis (FilterBasis.filter B) (fun s => s ∈ B) id

ink

theorem Filter.HasBasis.to_has_basis' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ (i' : ι'), p' i' → s' i' ∈ l) : Filter.HasBasis l p' s'

ink

theorem Filter.HasBasis.to_hasBasis {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') : Filter.HasBasis l p' s'

ink

theorem Filter.HasBasis.to_subset {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {t : ι → Set α} (h : ∀ (i : ι), p i → t i ⊆ s i) (ht : ∀ (i : ι), p i → t i ∈ l) : Filter.HasBasis l p t

ink

theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {q : α → Prop} : Filter.Eventually (fun x => q x) l ↔ ∃ i, p i ∧ (⦃x : α⦄ → x ∈ s i → q x)

ink

theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {q : α → Prop} : Filter.Frequently (fun x => q x) l ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x

ink

theorem Filter.HasBasis.exists_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {P : Set α → Prop} (mono : ⦃s t : Set α⦄ → s ⊆ t → P t → P s) : (∃ s, s ∈ l ∧ P s) ↔ ∃ i, p i ∧ P (s i)

ink

theorem Filter.HasBasis.forall_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {P : Set α → Prop} (mono : ⦃s t : Set α⦄ → s ⊆ t → P s → P t) : ((s : Set α) → s ∈ l → P s) ↔ (i : ι) → p i → P (s i)

ink

theorem Filter.HasBasis.neBot_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : Filter.NeBot l ↔ ∀ {i : ι}, p i → Set.Nonempty (s i)

ink

theorem Filter.HasBasis.eq_bot_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : l = ⊥ ↔ ∃ i, p i ∧ s i = ∅

ink

theorem Filter.generate_neBot_iff {α : Type u_1} {s : Set (Set α)} : Filter.NeBot (Filter.generate s) ↔ ∀ (t : Set (Set α)), t ⊆ s → Set.Finite t → Set.Nonempty (⋂₀ t)

ink

theorem Filter.basis_sets {α : Type u_1} (l : Filter α) : Filter.HasBasis l (fun s => s ∈ l) id

ink

theorem Filter.asBasis_filter {α : Type u_1} (f : Filter α) : FilterBasis.filter (Filter.asBasis f) = f

ink

theorem Filter.hasBasis_self {α : Type u_1} {l : Filter α} {P : Set α → Prop} : Filter.HasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ (t : Set α), t ∈ l → ∃ r, r ∈ l ∧ P r ∧ r ⊆ t

ink

theorem Filter.HasBasis.comp_surjective {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {g : ι' → ι} (hg : Function.Surjective g) : Filter.HasBasis l (p ∘ g) (s ∘ g)

ink

theorem Filter.HasBasis.comp_equiv {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) (e : ι' ≃ ι) : Filter.HasBasis l (p ∘ ↑e) (s ∘ ↑e)

ink

theorem Filter.HasBasis.restrict {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {q : ι → Prop} (hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) : Filter.HasBasis l (fun i => p i ∧ q i) s

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∧ q j, then {s j | p j ∧ q j}∧ q j} is a basis of l.

ink

theorem Filter.HasBasis.restrict_subset {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {V : Set α} (hV : V ∈ l) : Filter.HasBasis l (fun i => p i ∧ s i ⊆ V) s

If {s i | p i} is a basis of a filter l and V ∈ l∈ l, then {s i | p i ∧ s i ⊆ V}∧ s i ⊆ V}⊆ V} is a basis of l.

ink

theorem Filter.HasBasis.hasBasis_self_subset {α : Type u_1} {l : Filter α} {p : Set α → Prop} (h : Filter.HasBasis l (fun s => s ∈ l ∧ p s) id) {V : Set α} (hV : V ∈ l) : Filter.HasBasis l (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id

ink

theorem Filter.HasBasis.ge_iff {α : Type u_1} {ι' : Sort u_2} {l : Filter α} {l' : Filter α} {p' : ι' → Prop} {s' : ι' → Set α} (hl' : Filter.HasBasis l' p' s') : l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l

ink

theorem Filter.HasBasis.le_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : l ≤ l' ↔ ∀ (t : Set α), t ∈ l' → ∃ i, p i ∧ s i ⊆ t

ink

theorem Filter.HasBasis.le_basis_iff {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

ink

theorem Filter.HasBasis.ext {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') (h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l = l'

ink

theorem Filter.HasBasis.inf' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊓ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd

ink

theorem Filter.HasBasis.inf {α : Type u_3} {l : Filter α} {l' : Filter α} {ι : Type u_1} {ι' : Type u_2} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊓ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd

ink

theorem Filter.hasBasis_infᵢ' {α : Type u_3} {ι : Type u_1} {ι' : ι → Type u_2} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨅ i, l i) (fun If => Set.Finite If.fst ∧ ((i : ι) → i ∈ If.fst → p i (Prod.snd (Set ι) ((i : ι) → ι' i) If i))) fun If => Set.interᵢ fun i => Set.interᵢ fun h => s i (Prod.snd (Set ι) ((i : ι) → ι' i) If i)

ink

theorem Filter.hasBasis_infᵢ {α : Type u_3} {ι : Type u_1} {ι' : ι → Type u_2} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨅ i, l i) (fun If => Set.Finite If.fst ∧ ((i : ↑If.fst) → p (↑i) (Sigma.snd (Set ι) (fun I => (i : ↑I) → ι' ↑i) If i))) fun If => Set.interᵢ fun i => s (↑i) (Sigma.snd (Set ι) (fun I => (i : ↑I) → ι' ↑i) If i)

ink

theorem Filter.hasBasis_infᵢ_of_directed' {α : Type u_3} {ι : Type u_1} {ι' : ι → Type u_2} [inst : Nonempty ι] {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop) (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) (h : Directed (fun x x_1 => x ≥ x_1) l) : Filter.HasBasis (⨅ i, l i) (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

ink

theorem Filter.hasBasis_infᵢ_of_directed {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) (h : Directed (fun x x_1 => x ≥ x_1) l) : Filter.HasBasis (⨅ i, l i) (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

ink

theorem Filter.hasBasis_binfᵢ_of_directed' {α : Type u_3} {ι : Type u_1} {ι' : ι → Type u_2} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop) (hl : ∀ (i : ι), i ∈ dom → Filter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) : Filter.HasBasis (⨅ i, ⨅ h, l i) (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

ink

theorem Filter.hasBasis_binfᵢ_of_directed {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), i ∈ dom → Filter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) : Filter.HasBasis (⨅ i, ⨅ h, l i) (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

ink

theorem Filter.hasBasis_principal {α : Type u_1} (t : Set α) : Filter.HasBasis (Filter.principal t) (fun x => True) fun x => t

ink

theorem Filter.hasBasis_pure {α : Type u_1} (x : α) : Filter.HasBasis (pure x) (fun x => True) fun x => {x}

ink

theorem Filter.HasBasis.sup' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊔ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd

ink

theorem Filter.HasBasis.sup {α : Type u_3} {l : Filter α} {l' : Filter α} {ι : Type u_1} {ι' : Type u_2} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊔ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd

ink

theorem Filter.hasBasis_supᵢ {α : Type u_3} {ι : Sort u_1} {ι' : ι → Type u_2} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨆ i, l i) (fun f => (i : ι) → p i (f i)) fun f => Set.unionᵢ fun i => s i (f i)

ink

theorem Filter.HasBasis.sup_principal {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (t : Set α) : Filter.HasBasis (l ⊔ Filter.principal t) p fun i => s i ∪ t

ink

theorem Filter.HasBasis.sup_pure {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (x : α) : Filter.HasBasis (l ⊔ pure x) p fun i => s i ∪ {x}

ink

theorem Filter.HasBasis.inf_principal {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (s' : Set α) : Filter.HasBasis (l ⊓ Filter.principal s') p fun i => s i ∩ s'

ink

theorem Filter.HasBasis.principal_inf {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (s' : Set α) : Filter.HasBasis (Filter.principal s' ⊓ l) p fun i => s' ∩ s i

ink

theorem Filter.HasBasis.inf_basis_neBot_iff {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → Set.Nonempty (s i ∩ s' i')

ink

theorem Filter.HasBasis.inf_neBot_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : Set α⦄, s' ∈ l' → Set.Nonempty (s i ∩ s')

ink

theorem Filter.HasBasis.inf_principal_neBot_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {t : Set α} : Filter.NeBot (l ⊓ Filter.principal t) ↔ ∀ ⦃i : ι⦄, p i → Set.Nonempty (s i ∩ t)

ink

theorem Filter.HasBasis.disjoint_iff {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

ink

theorem Disjoint.exists_mem_filter_basis {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (h : Disjoint l l') (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

ink

theorem Pairwise.exists_mem_filter_basis_of_disjoint {α : Type u_2} {I : Type u_1} [inst : Finite I] {l : I → Filter α} {ι : I → Sort u_3} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} (hd : Pairwise (Disjoint on l)) (h : ∀ (i : I), Filter.HasBasis (l i) (p i) (s i)) : ∃ ind, ((i : I) → p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

ink

theorem Set.PairwiseDisjoint.exists_mem_filter_basis {α : Type u_2} {I : Type u_1} {l : I → Filter α} {ι : I → Sort u_3} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} {S : Set I} (hd : Set.PairwiseDisjoint S l) (hS : Set.Finite S) (h : ∀ (i : I), Filter.HasBasis (l i) (p i) (s i)) : ∃ ind, ((i : I) → p i (ind i)) ∧ Set.PairwiseDisjoint S fun i => s i (ind i)

ink

theorem Filter.inf_neBot_iff {α : Type u_1} {l : Filter α} {l' : Filter α} : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s' : Set α⦄, s' ∈ l' → Set.Nonempty (s ∩ s')

ink

theorem Filter.inf_principal_neBot_iff {α : Type u_1} {l : Filter α} {s : Set α} : Filter.NeBot (l ⊓ Filter.principal s) ↔ ∀ (U : Set α), U ∈ l → Set.Nonempty (U ∩ s)

ink

theorem Filter.mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} : s ∈ f ↔ f ⊓ Filter.principal (sᶜ) = ⊥

ink

theorem Filter.not_mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} : ¬s ∈ f ↔ Filter.NeBot (f ⊓ Filter.principal (sᶜ))

ink

@[simp]

theorem Filter.disjoint_principal_right {α : Type u_1} {f : Filter α} {s : Set α} : Disjoint f (Filter.principal s) ↔ sᶜ ∈ f

ink

@[simp]

theorem Filter.disjoint_principal_left {α : Type u_1} {f : Filter α} {s : Set α} : Disjoint (Filter.principal s) f ↔ sᶜ ∈ f

ink

@[simp]

theorem Filter.disjoint_principal_principal {α : Type u_1} {s : Set α} {t : Set α} : Disjoint (Filter.principal s) (Filter.principal t) ↔ Disjoint s t

ink

theorem Disjoint.filter_principal {α : Type u_1} {s : Set α} {t : Set α} : Disjoint s t → Disjoint (Filter.principal s) (Filter.principal t)

Alias of the reverse direction of Filter.disjoint_principal_principal.

ink

@[simp]

theorem Filter.disjoint_pure_pure {α : Type u_1} {x : α} {y : α} : Disjoint (pure x) (pure y) ↔ x ≠ y

ink

@[simp]

theorem Filter.compl_diagonal_mem_prod {α : Type u_1} {l₁ : Filter α} {l₂ : Filter α} : Set.diagonal αᶜ ∈ Filter.prod l₁ l₂ ↔ Disjoint l₁ l₂

ink

theorem Filter.HasBasis.disjoint_iff_left {α : Type u_1} {ι : Sort u_2} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Disjoint l l' ↔ ∃ i, p i ∧ s iᶜ ∈ l'

ink

theorem Filter.HasBasis.disjoint_iff_right {α : Type u_1} {ι : Sort u_2} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Disjoint l' l ↔ ∃ i, p i ∧ s iᶜ ∈ l'

ink

theorem Filter.le_iff_forall_inf_principal_compl {α : Type u_1} {f : Filter α} {g : Filter α} : f ≤ g ↔ ∀ (V : Set α), V ∈ g → f ⊓ Filter.principal (Vᶜ) = ⊥

ink

theorem Filter.inf_neBot_iff_frequently_left {α : Type u_1} {f : Filter α} {g : Filter α} : Filter.NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, Filter.Eventually (fun x => p x) f → Filter.Frequently (fun x => p x) g

ink

theorem Filter.inf_neBot_iff_frequently_right {α : Type u_1} {f : Filter α} {g : Filter α} : Filter.NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, Filter.Eventually (fun x => p x) g → Filter.Frequently (fun x => p x) f

ink

theorem Filter.HasBasis.eq_binfᵢ {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : l = ⨅ i, ⨅ _hi, Filter.principal (s i)

ink

theorem Filter.HasBasis.eq_infᵢ {α : Type u_1} {ι : Sort u_2} {l : Filter α} {s : ι → Set α} (h : Filter.HasBasis l (fun x => True) s) : l = ⨅ i, Filter.principal (s i)

ink

theorem Filter.hasBasis_infᵢ_principal {α : Type u_1} {ι : Sort u_2} {s : ι → Set α} (h : Directed (fun x x_1 => x ≥ x_1) s) [inst : Nonempty ι] : Filter.HasBasis (⨅ i, Filter.principal (s i)) (fun x => True) s

ink

theorem Filter.hasBasis_infᵢ_principal_finite {α : Type u_2} {ι : Type u_1} (s : ι → Set α) : Filter.HasBasis (⨅ i, Filter.principal (s i)) (fun t => Set.Finite t) fun t => Set.interᵢ fun i => Set.interᵢ fun h => s i

If s : ι → Set α→ Set α is an indexed family of sets, then finite intersections of s i form a basis of ⨅ i, 𝓟 (s i)⨅ i, 𝓟 (s i).

ink

theorem Filter.hasBasis_binfᵢ_principal {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S) (ne : Set.Nonempty S) : Filter.HasBasis (⨅ i, ⨅ h, Filter.principal (s i)) (fun i => i ∈ S) s

ink

theorem Filter.hasBasis_binfᵢ_principal' {α : Type u_2} {ι : Type u_1} {p : ι → Prop} {s : ι → Set α} (h : ∀ (i : ι), p i → ∀ (j : ι), p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j) (ne : ∃ i, p i) : Filter.HasBasis (⨅ i, ⨅ _h, Filter.principal (s i)) p s

ink

theorem Filter.HasBasis.map {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β) (hl : Filter.HasBasis l p s) : Filter.HasBasis (Filter.map f l) p fun i => f '' s i

ink

theorem Filter.HasBasis.comap {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α) (hl : Filter.HasBasis l p s) : Filter.HasBasis (Filter.comap f l) p fun i => f ⁻¹' s i

ink

theorem Filter.comap_hasBasis {α : Type u_2} {β : Type u_1} (f : α → β) (l : Filter β) : Filter.HasBasis (Filter.comap f l) (fun s => s ∈ l) fun s => f ⁻¹' s

ink

theorem Filter.HasBasis.forall_mem_mem {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {x : α} : (∀ (t : Set α), t ∈ l → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

ink

theorem Filter.HasBasis.binfᵢ_mem {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} [inst : CompleteLattice β] {f : Set α → β} (h : Filter.HasBasis l p s) (hf : Monotone f) : (⨅ t, ⨅ h, f t) = ⨅ i, ⨅ _hi, f (s i)

ink

theorem Filter.HasBasis.binterᵢ_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {f : Set α → Set β} (h : Filter.HasBasis l p s) (hf : Monotone f) : (Set.interᵢ fun t => Set.interᵢ fun h => f t) = Set.interᵢ fun i => Set.interᵢ fun _hi => f (s i)

ink

theorem Filter.HasBasis.interₛ_sets {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : ⋂₀ l.sets = Set.interᵢ fun i => Set.interᵢ fun _hi => s i

ink

structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_2} [inst : Preorder ι''] (s'' : ι'' → Set α) extends Filter.IsBasis : Prop

• The sequence of sets is antitone.

  antitone : Antitone s''

IsAntitoneBasis s means the image of s is a filter basis such that s is decreasing.

ink

structure Filter.HasAntitoneBasis {α : Type u_1} {ι'' : Type u_2} [inst : Preorder ι''] (l : Filter α) (s : ι'' → Set α) extends Filter.HasBasis : Prop

• The sequence of sets is antitone.

  antitone : Antitone s

We say that a filter l has an antitone basis s : ι → Set α→ Set α, if t ∈ l∈ l if and only if t includes s i for some i, and s is decreasing.

ink

theorem Filter.HasAntitoneBasis.map {α : Type u_1} {β : Type u_3} {ι'' : Type u_2} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α} {m : α → β} (hf : Filter.HasAntitoneBasis l s) : Filter.HasAntitoneBasis (Filter.map m l) fun n => m '' s n

ink

theorem Filter.HasBasis.tendsto_left_iff {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {f : α → β} (hla : Filter.HasBasis la pa sa) : Filter.Tendsto f la lb ↔ ∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ Set.MapsTo f (sa i) t

ink

theorem Filter.HasBasis.tendsto_right_iff {α : Type u_3} {β : Type u_1} {ι' : Sort u_2} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (hlb : Filter.HasBasis lb pb sb) : Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → Filter.Eventually (fun x => f x ∈ sb i) la

ink

theorem Filter.HasBasis.tendsto_iff {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {ι' : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ (x : α), x ∈ sa ia → f x ∈ sb ib

ink

theorem Filter.Tendsto.basis_left {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {f : α → β} (H : Filter.Tendsto f la lb) (hla : Filter.HasBasis la pa sa) (t : Set β) : t ∈ lb → ∃ i, pa i ∧ Set.MapsTo f (sa i) t

ink

theorem Filter.Tendsto.basis_right {α : Type u_1} {β : Type u_2} {ι' : Sort u_3} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (H : Filter.Tendsto f la lb) (hlb : Filter.HasBasis lb pb sb) (i : ι') : pb i → Filter.Eventually (fun x => f x ∈ sb i) la

ink

theorem Filter.Tendsto.basis_both {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {ι' : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (H : Filter.Tendsto f la lb) (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) (ib : ι') : pb ib → ∃ ia, pa ia ∧ Set.MapsTo f (sa ia) (sb ib)

ink

theorem Filter.HasBasis.prod_pprod {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {ι' : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (Filter.prod la lb) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd

ink

theorem Filter.HasBasis.prod {α : Type u_3} {β : Type u_4} {la : Filter α} {lb : Filter β} {ι : Type u_1} {ι' : Type u_2} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (Filter.prod la lb) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd

ink

theorem Filter.HasBasis.prod_same_index {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {la : Filter α} {sa : ι → Set α} {lb : Filter β} {p : ι → Prop} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) : Filter.HasBasis (Filter.prod la lb) p fun i => sa i ×ˢ sb i

ink

theorem Filter.HasBasis.prod_same_index_mono {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {ι : Type u_1} [inst : LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (hsa : MonotoneOn sa { i | p i }) (hsb : MonotoneOn sb { i | p i }) : Filter.HasBasis (Filter.prod la lb) p fun i => sa i ×ˢ sb i

ink

theorem Filter.HasBasis.prod_same_index_anti {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {ι : Type u_1} [inst : LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (hsa : AntitoneOn sa { i | p i }) (hsb : AntitoneOn sb { i | p i }) : Filter.HasBasis (Filter.prod la lb) p fun i => sa i ×ˢ sb i

ink

theorem Filter.HasBasis.prod_self {α : Type u_1} {ι : Sort u_2} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (hl : Filter.HasBasis la pa sa) : Filter.HasBasis (Filter.prod la la) pa fun i => sa i ×ˢ sa i

ink

theorem Filter.mem_prod_self_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} : s ∈ Filter.prod la la ↔ ∃ t, t ∈ la ∧ t ×ˢ t ⊆ s

ink

theorem Filter.HasAntitoneBasis.prod {α : Type u_2} {β : Type u_3} {ι : Type u_1} [inst : LinearOrder ι] {f : Filter α} {g : Filter β} {s : ι → Set α} {t : ι → Set β} (hf : Filter.HasAntitoneBasis f s) (hg : Filter.HasAntitoneBasis g t) : Filter.HasAntitoneBasis (Filter.prod f g) fun n => s n ×ˢ t n

ink

theorem Filter.HasBasis.coprod {α : Type u_3} {β : Type u_4} {la : Filter α} {lb : Filter β} {ι : Type u_1} {ι' : Type u_2} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (Filter.coprod la lb) (fun i => pa i.fst ∧ pb i.snd) fun i => Prod.fst ⁻¹' sa i.fst ∪ Prod.snd ⁻¹' sb i.snd

ink

theorem Filter.map_sigma_mk_comap {α : Type u_3} {β : Type u_4} {π : α → Type u_1} {π' : β → Type u_2} {f : α → β} (hf : Function.Injective f) (g : (a : α) → π a → π' (f a)) (a : α) (l : Filter (π' (f a))) : Filter.map (Sigma.mk a) (Filter.comap (g a) l) = Filter.comap (Sigma.map f g) (Filter.map (Sigma.mk (f a)) l)

ink

class Filter.IsCountablyGenerated {α : Type u_1} (f : Filter α) : Prop

• There exists a countable set that generates the filter.

  out : ∃ s, Set.Countable s ∧ f = Filter.generate s

IsCountablyGenerated f means f = generate s for some countable s.

ink

structure Filter.IsCountableBasis {α : Type u_1} {ι : Type u_2} (p : ι → Prop) (s : ι → Set α) extends Filter.IsBasis : Prop

• The set of i that satisfy the predicate p is countable.

  countable : Set.Countable (setOf p)

IsCountableBasis p s means the image of s bounded by p is a countable filter basis.

ink

structure Filter.HasCountableBasis {α : Type u_1} {ι : Type u_2} (l : Filter α) (p : ι → Prop) (s : ι → Set α) extends Filter.HasBasis : Prop

• The set of i that satisfy the predicate p is countable.

  countable : Set.Countable (setOf p)

We say that a filter l has a countable basis s : ι → set α→ set α bounded by p : ι → Prop→ Prop, if t ∈ l∈ l if and only if t includes s i for some i such that p i, and the set defined by p is countable.

ink

structure Filter.CountableFilterBasis (α : Type u_1) extends FilterBasis : Type u_1

• The set of sets of the filter basis is countable.

  countable : Set.Countable toFilterBasis.sets

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.

ink

instance Filter.Nat.inhabitedCountableFilterBasis : Inhabited (Filter.CountableFilterBasis ℕ)

Equations

• Filter.Nat.inhabitedCountableFilterBasis = { default := { toFilterBasis := default, countable := Filter.Nat.inhabitedCountableFilterBasis.proof_1 } }

ink

theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_2} {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasCountableBasis f p s) : Filter.IsCountablyGenerated f

ink

theorem Filter.antitone_seq_of_seq {α : Type u_1} (s : ℕ → Set α) : ∃ t, Antitone t ∧ (⨅ i, Filter.principal (s i)) = ⨅ i, Filter.principal (t i)

ink

theorem Filter.countable_binfᵢ_eq_infᵢ_seq {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (Bne : Set.Nonempty B) (f : ι → α) : ∃ x, (⨅ t, ⨅ h, f t) = ⨅ i, f (x i)

ink

theorem Filter.countable_binfᵢ_eq_infᵢ_seq' {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) : ∃ x, (⨅ t, ⨅ h, f t) = ⨅ i, f (x i)

ink

theorem Filter.countable_binfᵢ_principal_eq_seq_infᵢ {α : Type u_1} {B : Set (Set α)} (Bcbl : Set.Countable B) : ∃ x, (⨅ t, ⨅ h, Filter.principal t) = ⨅ i, Filter.principal (x i)

ink

theorem Filter.HasAntitoneBasis.mem_iff {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) {t : Set α} : t ∈ l ↔ ∃ i, s i ⊆ t

ink

theorem Filter.HasAntitoneBasis.mem {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) (i : ι) : s i ∈ l

ink

theorem Filter.HasAntitoneBasis.hasBasis_ge {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] [inst : IsDirected ι fun x x_1 => x ≤ x_1] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) (i : ι) : Filter.HasBasis l (fun j => i ≤ j) s

ink

theorem Filter.HasBasis.exists_antitone_subbasis {α : Type u_1} {ι' : Sort u_2} {f : Filter α} [h : Filter.IsCountablyGenerated f] {p : ι' → Prop} {s : ι' → Set α} (hs : Filter.HasBasis f p s) : ∃ x, ((i : ℕ) → p (x i)) ∧ Filter.HasAntitoneBasis f fun i => s (x i)

If f is countably generated and f.HasBasis p s, then f admits a decreasing basis enumerated by natural numbers such that all sets have the form s i. More precisely, there is a sequence i n such that p (i n) for all n and s (i n) is a decreasing sequence of sets which forms a basis of f

ink

theorem Filter.exists_antitone_basis {α : Type u_1} (f : Filter α) [inst : Filter.IsCountablyGenerated f] : ∃ x, Filter.HasAntitoneBasis f x

A countably generated filter admits a basis formed by an antitone sequence of sets.

ink

theorem Filter.exists_antitone_seq {α : Type u_1} (f : Filter α) [inst : Filter.IsCountablyGenerated f] : ∃ x, Antitone x ∧ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s

ink

instance Filter.Inf.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [inst : Filter.IsCountablyGenerated f] [inst : Filter.IsCountablyGenerated g] : Filter.IsCountablyGenerated (f ⊓ g)

Equations

• @Filter.Inf.isCountablyGenerated = @Filter.Inf.isCountablyGenerated.proof_1

ink

instance Filter.map.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter α) [inst : Filter.IsCountablyGenerated l] (f : α → β) : Filter.IsCountablyGenerated (Filter.map f l)

Equations

• @Filter.map.isCountablyGenerated = @Filter.map.isCountablyGenerated.proof_1

ink

instance Filter.comap.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter β) [inst : Filter.IsCountablyGenerated l] (f : α → β) : Filter.IsCountablyGenerated (Filter.comap f l)

Equations

• @Filter.comap.isCountablyGenerated = @Filter.comap.isCountablyGenerated.proof_1

ink

instance Filter.Sup.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [inst : Filter.IsCountablyGenerated f] [inst : Filter.IsCountablyGenerated g] : Filter.IsCountablyGenerated (f ⊔ g)

Equations

• @Filter.Sup.isCountablyGenerated = @Filter.Sup.isCountablyGenerated.proof_1

ink

instance Filter.prod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [inst : Filter.IsCountablyGenerated la] [inst : Filter.IsCountablyGenerated lb] : Filter.IsCountablyGenerated (Filter.prod la lb)

Equations

• @Filter.prod.isCountablyGenerated = @Filter.prod.isCountablyGenerated.proof_1

ink

instance Filter.coprod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [inst : Filter.IsCountablyGenerated la] [inst : Filter.IsCountablyGenerated lb] : Filter.IsCountablyGenerated (Filter.coprod la lb)

Equations

• @Filter.coprod.isCountablyGenerated = @Filter.coprod.isCountablyGenerated.proof_1

ink

theorem Filter.isCountablyGenerated_seq {α : Type u_2} {β : Type u_1} [inst : Countable β] (x : β → Set α) : Filter.IsCountablyGenerated (⨅ i, Filter.principal (x i))

ink

theorem Filter.isCountablyGenerated_of_seq {α : Type u_1} {f : Filter α} (h : ∃ x, f = ⨅ i, Filter.principal (x i)) : Filter.IsCountablyGenerated f

ink

theorem Filter.isCountablyGenerated_binfᵢ_principal {α : Type u_1} {B : Set (Set α)} (h : Set.Countable B) : Filter.IsCountablyGenerated (⨅ s, ⨅ h, Filter.principal s)

ink

theorem Filter.isCountablyGenerated_iff_exists_antitone_basis {α : Type u_1} {f : Filter α} : Filter.IsCountablyGenerated f ↔ ∃ x, Filter.HasAntitoneBasis f x

ink

theorem Filter.isCountablyGenerated_principal {α : Type u_1} (s : Set α) : Filter.IsCountablyGenerated (Filter.principal s)

ink

theorem Filter.isCountablyGenerated_pure {α : Type u_1} (a : α) : Filter.IsCountablyGenerated (pure a)

ink

theorem Filter.isCountablyGenerated_bot {α : Type u_1} : Filter.IsCountablyGenerated ⊥

ink

theorem Filter.isCountablyGenerated_top {α : Type u_1} : Filter.IsCountablyGenerated ⊤

ink

instance Filter.infᵢ.isCountablyGenerated {ι : Sort u} {α : Type v} [inst : Countable ι] (f : ι → Filter α) [inst : ∀ (i : ι), Filter.IsCountablyGenerated (f i)] : Filter.IsCountablyGenerated (⨅ i, f i)

Equations

• @Filter.infᵢ.isCountablyGenerated = @Filter.infᵢ.isCountablyGenerated.proof_1