Basic results on 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, and a map s : ι → Set α, the proposition h : Filter.IsBasis p s makes sure the range of s bounded by p (i.e. s '' Set.ofPred p) defines a filter basis h.filterBasis.

If one already has a filter l on α, Filter.HasBasis 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.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) that returns some index i such that p i and s i ⊆ t. This function can be useful to avoid manual destruction of h.mem_iff.mpr ht using cases or let.

Main statements

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

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

• 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 ⊓ 𝓟 t, l ×ˢ l', l ×ˢ l, l.map f, l.comap f respectively;

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

Implementation notes

As with Set.iUnion/biUnion/Set.sUnion, there are three different approaches to filter bases:

• Filter.HasBasis l s, s : Set (Set α);
• Filter.HasBasis l s, s : ι → Set α;
• Filter.HasBasis l p s, p : ι → Prop, s : ι → Set α.

We use the latter one because, e.g., 𝓝 x in an EMetricSpace or in a MetricSpace has a basis of this form. The other two can be emulated using s = id or p = fun _ ↦ True.

With this approach sometimes one needs to simp the statement provided by the Filter.HasBasis machinery, e.g., simp only [true_and_iff] or simp only [forall_const] can help with the case p = fun _ ↦ True.

Main statements

structure FilterBasis (α : Type u_5) : Type u_5

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.

• sets : Set (Set α)

  Sets of a filter basis.

• nonempty : self.sets.Nonempty

  The set of filter basis sets is nonempty.

• inter_sets {x y : Set α} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y

  The set of filter basis sets is directed downwards.

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

@[instance_reducible]

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

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

Equations

• instMembershipSetFilterBasis = { mem := fun (B : FilterBasis α) (U : Set α) => U ∈ B.sets }

@[simp]

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

@[instance_reducible]

instance instInhabitedFilterBasisNat : Inhabited (FilterBasis ℕ)

Equations

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

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

View a filter as a filter basis.

Equations

• f.asBasis = { sets := f.sets, nonempty := ⋯, inter_sets := ⋯ }

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

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

• nonempty : ∃ (i : ι), p i

  There exists at least one i that satisfies p.

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

  s is directed downwards on i such that p i.

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

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

Equations

• h.filterBasis = { sets := {t : Set α | ∃ (i : ι), p i ∧ s i = t}, nonempty := ⋯, inter_sets := ⋯ }

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

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

The filter associated to a filter basis.

Equations

• B.filter = { sets := {s : Set α | ∃ t ∈ B, t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

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

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

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

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

theorem FilterBasis.ker_filter {α : Type u_1} (F : FilterBasis α) : F.filter.ker = ⋂₀ F.sets

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

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

Equations

• h.filter = h.filterBasis.filter

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

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

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

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.

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

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

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

Definition of HasBasis unfolded with implicit set argument.

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

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

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

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

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

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

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

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

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

Equations

• h.index t ht = ⟨⋯.choose, ⋯⟩

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

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

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

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

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

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

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

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

theorem Filter.HasBasis.to_hasBasis {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis 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.HasBasis p' s'

theorem Filter.HasBasis.congr {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {p' : ι → Prop} {s' : ι → Set α} (hp : ∀ (i : ι), p i ↔ p' i) (hs : ∀ (i : ι), p i → s i = s' i) : l.HasBasis p' s'

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

theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {q : α → Prop} : (∀ᶠ (x : α) in l, q x) ↔ ∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x

theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {q : α → Prop} : (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

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

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

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

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

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

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

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

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

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

theorem Filter.HasBasis.to_image_id' {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l.HasBasis (fun (t : Set α) => ∃ (i : ι), p i ∧ s i = t) id

theorem Filter.HasBasis.to_image_id {α : Type u_1} {l : Filter α} {ι : Type u_5} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l.HasBasis (fun (x : Set α) => x ∈ s '' {i : ι | p i}) id

theorem Filter.HasBasis.restrict {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) {q : ι → Prop} (hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i) : l.HasBasis (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, then {s j | p j ∧ q j} is a basis of l.

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

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.

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

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

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

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

theorem Filter.HasBasis.eq_top_iff {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l = ⊤ ↔ ∀ (i : ι), p i → s i = Set.univ

theorem Filter.HasBasis.ext {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s) (hl' : l'.HasBasis 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'

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

theorem Filter.HasBasis.inf {α : Type u_1} {l l' : Filter α} {ι : Type u_5} {ι' : Type u_6} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : (l ⊓ l').HasBasis (fun (i : ι × ι') => p i.1 ∧ p' i.2) fun (i : ι × ι') => s i.1 ∩ s' i.2

theorem Filter.hasBasis_iInf_of_directed' {α : Type u_1} {ι : Type u_5} {ι' : ι → Type u_6} [Nonempty ι] {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop) (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) (h : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) l) : (⨅ (i : ι), l i).HasBasis (fun (ii' : (i : ι) × ι' i) => p ii'.fst ii'.snd) fun (ii' : (i : ι) × ι' i) => s ii'.fst ii'.snd

theorem Filter.hasBasis_iInf_of_directed {α : Type u_1} {ι : Type u_5} {ι' : Type u_6} [Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) (h : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) l) : (⨅ (i : ι), l i).HasBasis (fun (ii' : ι × ι') => p ii'.1 ii'.2) fun (ii' : ι × ι') => s ii'.1 ii'.2

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

theorem Filter.hasBasis_biInf_of_directed {α : Type u_1} {ι : Type u_5} {ι' : Type u_6} {dom : Set ι} (hdom : dom.Nonempty) {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) : (⨅ i ∈ dom, l i).HasBasis (fun (ii' : ι × ι') => ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun (ii' : ι × ι') => s ii'.1 ii'.2

theorem Filter.hasBasis_top {α : Type u_1} : ⊤.HasBasis (fun (x : Unit) => True) fun (x : Unit) => Set.univ

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

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

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

theorem Filter.HasBasis.sup {α : Type u_1} {l l' : Filter α} {ι : Type u_5} {ι' : Type u_6} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : (l ⊔ l').HasBasis (fun (i : ι × ι') => p i.1 ∧ p' i.2) fun (i : ι × ι') => s i.1 ∪ s' i.2

theorem Filter.hasBasis_iSup {α : Type u_1} {ι : Sort u_5} {ι' : ι → Type u_6} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) : (⨆ (i : ι), l i).HasBasis (fun (f : (i : ι) → ι' i) => ∀ (i : ι), p i (f i)) fun (f : (i : ι) → ι' i) => ⋃ (i : ι), s i (f i)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Filter.notMem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} : s ∉ f ↔ (f ⊓ principal sᶜ).NeBot

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Filter.disjoint_principal_principal.

@[simp]

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

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

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

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

theorem Filter.inf_neBot_iff_frequently_left {α : Type u_1} {f g : Filter α} : (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

theorem Filter.inf_neBot_iff_frequently_right {α : Type u_1} {f g : Filter α} : (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

theorem Filter.HasBasis.eq_biInf {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l = ⨅ (i : ι), ⨅ (_ : p i), principal (s i)

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

theorem Filter.hasBasis_iInf_principal {α : Type u_1} {ι : Sort u_3} {s : ι → Set α} (h : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) [Nonempty ι] : (⨅ (i : ι), principal (s i)).HasBasis (fun (x : ι) => True) s

theorem Filter.hasBasis_biInf_principal {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) => x1 ⊇ x2) S) (ne : S.Nonempty) : (⨅ i ∈ S, principal (s i)).HasBasis (fun (i : β) => i ∈ S) s

theorem Filter.hasBasis_biInf_principal' {α : Type u_1} {ι : Type u_5} {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) : (⨅ (i : ι), ⨅ (_ : p i), principal (s i)).HasBasis p s

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

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

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

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

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

theorem Filter.HasBasis.biInter_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {f : Set α → Set β} (h : l.HasBasis p s) (hf : Monotone f) : ⋂ t ∈ l, f t = ⋂ (i : ι), ⋂ (_ : p i), f (s i)

theorem Filter.HasBasis.ker {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l.ker = ⋂ (i : ι), ⋂ (_ : p i), s i

structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_5} [Preorder ι''] (s'' : ι'' → Set α) extends Filter.IsBasis (fun (x : ι'') => True) s'' : Prop

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

• nonempty : ∃ (i : ι''), True
• inter {i j : ι''} : True → True → ∃ (k : ι''), True ∧ s'' k ⊆ s'' i ∩ s'' j
• antitone : Antitone s''

  The sequence of sets is antitone.

structure Filter.HasAntitoneBasis {α : Type u_1} {ι'' : Type u_5} [Preorder ι''] (l : Filter α) (s : ι'' → Set α) extends l.HasBasis (fun (x : ι'') => True) s : Prop

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

• mem_iff' (t : Set α) : t ∈ l ↔ ∃ (i : ι''), True ∧ s i ⊆ t
• antitone : Antitone s

  The sequence of sets is antitone.

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

theorem Filter.HasAntitoneBasis.comap {α : Type u_1} {β : Type u_2} {ι'' : Type u_5} [Preorder ι''] {l : Filter α} {s : ι'' → Set α} (hf : l.HasAntitoneBasis s) (m : β → α) : (comap m l).HasAntitoneBasis fun (x : ι'') => m ⁻¹' s x

theorem Filter.HasAntitoneBasis.iInf_principal {α : Type u_1} {ι : Type u_6} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι] {s : ι → Set α} (hs : Antitone s) : (⨅ (i : ι), principal (s i)).HasAntitoneBasis s

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

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

theorem Filter.HasBasis.tendsto_iff {α : 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 : α → β} (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) : Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ (ia : ι), pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

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

theorem Filter.Tendsto.basis_right {α : Type u_1} {β : Type u_2} {ι' : Sort u_4} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (H : Tendsto f la lb) (hlb : lb.HasBasis pb sb) (i : ι') : pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

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 : Tendsto f la lb) (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) (ib : ι') : pb ib → ∃ (ia : ι), pa ia ∧ Set.MapsTo f (sa ia) (sb ib)

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

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

theorem Filter.HasBasis.principal_prod {α : Type u_1} {β : Type u_2} {ι' : Sort u_4} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (sa : Set α) (h : lb.HasBasis pb sb) : (principal sa ×ˢ lb).HasBasis pb fun (x : ι') => sa ×ˢ sb x

theorem Filter.HasBasis.prod_principal {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (h : la.HasBasis pa sa) (sb : Set β) : (la ×ˢ principal sb).HasBasis pa fun (x : ι) => sa x ×ˢ sb

theorem Filter.HasBasis.top_prod {α : Type u_1} {β : Type u_2} {ι' : Sort u_4} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (h : lb.HasBasis pb sb) : (⊤ ×ˢ lb).HasBasis pb fun (x : ι') => Set.univ ×ˢ sb x

theorem Filter.HasBasis.prod_top {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (h : la.HasBasis pa sa) : (la ×ˢ ⊤).HasBasis pa fun (x : ι) => sa x ×ˢ Set.univ

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

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

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

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

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

theorem Filter.eventually_prod_self_iff {α : Type u_1} {la : Filter α} {r : α → α → Prop} : (∀ᶠ (x : α × α) in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

theorem Filter.eventually_prod_self_iff' {α : Type u_1} {la : Filter α} {r : α × α → Prop} : (∀ᶠ (x : α × α) in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y)

A version of eventually_prod_self_iff that is more suitable for forward rewriting.

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

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

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