# 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 '' setOf 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 #

source
structure FilterBasis (α : Type u_6) :
Type u_6

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.

Instances For

source
instance FilterBasis.nonempty_sets {α : Type u_1} (B : FilterBasis α) :
Nonempty ↑B.sets
source
instance instMembershipSetFilterBasis {α : Type u_6} :
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 }

source
@[simp]
theorem FilterBasis.mem_sets {α : Type u_1} {s : Set α} {B : FilterBasis α} :
s ∈ B.sets ↔ s ∈ B
source
instance instInhabitedFilterBasisNat :
Inhabited (FilterBasis ℕ)
Equations

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

source
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 := ⋯ }

Instances For

source
structure Filter.IsBasis {α : Type u_1} {ι : Sort u_4} (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`.

Instances For

source
def Filter.IsBasis.filterBasis {α : Type u_1} {ι : Sort u_4} {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 := ⋯ }

Instances For

source
theorem Filter.IsBasis.mem_filterBasis_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) {U : Set α} :
U ∈ h.filterBasis ↔ ∃ (i : ι), p i ∧ s i = U
source
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 := ⋯ }

Instances For

source
theorem FilterBasis.mem_filter_iff {α : Type u_1} (B : FilterBasis α) {U : Set α} :
U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U
source
theorem FilterBasis.mem_filter_of_mem {α : Type u_1} (B : FilterBasis α) {U : Set α} :
U ∈ B → U ∈ B.filter
source
theorem FilterBasis.eq_iInf_principal {α : Type u_1} (B : FilterBasis α) :
B.filter = ⨅ (s : ↑B.sets), Filter.principal ↑s
source
theorem FilterBasis.generate {α : Type u_1} (B : FilterBasis α) :
Filter.generate B.sets = B.filter
source
theorem FilterBasis.ker_filter {α : Type u_1} (F : FilterBasis α) :
F.filter.ker = ⋂₀ F.sets
source
def Filter.IsBasis.filter {α : Type u_1} {ι : Sort u_4} {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

Instances For

source
theorem Filter.IsBasis.mem_filter_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) {U : Set α} :
U ∈ h.filter ↔ ∃ (i : ι), p i ∧ s i ⊆ U
source
theorem Filter.IsBasis.filter_eq_generate {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) :
h.filter = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
source
structure Filter.HasBasis {α : Type u_1} {ι : Sort u_4} (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.

Instances For

source
theorem Filter.HasBasis.mem_iff {α : Type u_1} {ι : Sort u_4} {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.

source
theorem Filter.HasBasis.eq_of_same_basis {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) (hl' : l'.HasBasis p s) :
l = l'
source
theorem Filter.hasBasis_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} :
l.HasBasis p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ (i : ι), p i ∧ s i ⊆ t
source
theorem Filter.HasBasis.ex_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
∃ (i : ι), p i
source
theorem Filter.HasBasis.nonempty {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
Nonempty ι
source
theorem Filter.IsBasis.hasBasis {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) :
h.filter.HasBasis p s
source
theorem Filter.HasBasis.mem_of_superset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} {i : ι} (hl : l.HasBasis p s) (hi : p i) (ht : s i ⊆ t) :
t ∈ l
source
theorem Filter.HasBasis.mem_of_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {i : ι} (hl : l.HasBasis p s) (hi : p i) :
s i ∈ l
source
noncomputable def Filter.HasBasis.index {α : Type u_1} {ι : Sort u_4} {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, ⋯⟩

Instances For

source
theorem Filter.HasBasis.property_index {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s) (ht : t ∈ l) :
p ↑(h.index t ht)
source
theorem Filter.HasBasis.set_index_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s) (ht : t ∈ l) :
s ↑(h.index t ht) ∈ l
source
theorem Filter.HasBasis.set_index_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s) (ht : t ∈ l) :
s ↑(h.index t ht) ⊆ t
source
theorem Filter.HasBasis.isBasis {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
IsBasis p s
source
theorem Filter.HasBasis.filter_eq {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
⋯.filter = l
source
theorem Filter.HasBasis.eq_generate {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
l = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
source
theorem FilterBasis.hasBasis {α : Type u_1} (B : FilterBasis α) :
B.filter.HasBasis (fun (s : Set α) => s ∈ B) id
source
theorem Filter.HasBasis.to_hasBasis' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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'
source
theorem Filter.HasBasis.to_hasBasis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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'
source
theorem Filter.HasBasis.congr {α : Type u_1} {ι : Sort u_4} {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'
source
theorem Filter.HasBasis.to_subset {α : Type u_1} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.exists_iff {α : Type u_1} {ι : Sort u_4} {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)
source
theorem Filter.HasBasis.forall_iff {α : Type u_1} {ι : Sort u_4} {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)
source
theorem Filter.HasBasis.neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) :
l.NeBot ↔ ∀ {i : ι}, p i → (s i).Nonempty
source
theorem Filter.HasBasis.eq_bot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) :
l = ⊥ ↔ ∃ (i : ι), p i ∧ s i = ∅
source
theorem Filter.basis_sets {α : Type u_1} (l : Filter α) :
l.HasBasis (fun (s : Set α) => s ∈ l) id
source
theorem Filter.asBasis_filter {α : Type u_1} (f : Filter α) :
f.asBasis.filter = f
source
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
source
theorem Filter.HasBasis.comp_surjective {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) {g : ι' → ι} (hg : Function.Surjective g) :
l.HasBasis (p ∘ g) (s ∘ g)
source
theorem Filter.HasBasis.comp_equiv {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) (e : ι' ≃ ι) :
l.HasBasis (p ∘ ⇑e) (s ∘ ⇑e)
source
theorem Filter.HasBasis.to_image_id' {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
l.HasBasis (fun (t : Set α) => ∃ (i : ι), p i ∧ s i = t) id
source
theorem Filter.HasBasis.to_image_id {α : Type u_1} {l : Filter α} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
l.HasBasis (fun (x : Set α) => x ∈ s '' {i : ι | p i}) id
source
theorem Filter.HasBasis.restrict {α : Type u_1} {ι : Sort u_4} {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`.

source
theorem Filter.HasBasis.restrict_subset {α : Type u_1} {ι : Sort u_4} {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`.

source
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
source
theorem Filter.HasBasis.ge_iff {α : Type u_1} {ι' : Sort u_5} {l l' : Filter α} {p' : ι' → Prop} {s' : ι' → Set α} (hl' : l'.HasBasis p' s') :
l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l
source
theorem Filter.HasBasis.le_iff {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) :
l ≤ l' ↔ ∀ t ∈ l', ∃ (i : ι), p i ∧ s i ⊆ t
source
theorem Filter.HasBasis.le_basis_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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'
source
theorem Filter.HasBasis.ext {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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'
source
theorem Filter.HasBasis.inf' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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
source
theorem Filter.HasBasis.inf {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {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
source
theorem Filter.hasBasis_iInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} [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
source
theorem Filter.hasBasis_iInf_of_directed {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} [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
source
theorem Filter.hasBasis_biInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {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
source
theorem Filter.hasBasis_biInf_of_directed {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {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
source
theorem Filter.hasBasis_top {α : Type u_1} :
⊤.HasBasis (fun (x : Unit) => True) fun (x : Unit) => Set.univ
source
theorem Filter.hasBasis_principal {α : Type u_1} (t : Set α) :
(principal t).HasBasis (fun (x : Unit) => True) fun (x : Unit) => t
source
theorem Filter.hasBasis_pure {α : Type u_1} (x : α) :
(pure x).HasBasis (fun (x : Unit) => True) fun (x_1 : Unit) => {x}
source
theorem Filter.HasBasis.sup' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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
source
theorem Filter.HasBasis.sup {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {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
source
theorem Filter.hasBasis_iSup {α : Type u_1} {ι : Sort u_6} {ι' : ι → Type u_7} {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)
source
theorem Filter.HasBasis.sup_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) (t : Set α) :
(l ⊔ principal t).HasBasis p fun (i : ι) => s i ∪ t
source
theorem Filter.HasBasis.sup_pure {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) (x : α) :
(l ⊔ pure x).HasBasis p fun (i : ι) => s i ∪ {x}
source
theorem Filter.HasBasis.inf_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) (s' : Set α) :
(l ⊓ principal s').HasBasis p fun (i : ι) => s i ∩ s'
source
theorem Filter.HasBasis.principal_inf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) (s' : Set α) :
(principal s' ⊓ l).HasBasis p fun (i : ι) => s' ∩ s i
source
theorem Filter.HasBasis.inf_basis_neBot_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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
source
theorem Filter.HasBasis.inf_neBot_iff {α : Type u_1} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.inf_principal_neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {t : Set α} :
(l ⊓ principal t).NeBot ↔ ∀ ⦃i : ι⦄, p i → (s i ∩ t).Nonempty
source
theorem Filter.HasBasis.disjoint_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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')
source
theorem Disjoint.exists_mem_filter_basis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {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')
source
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
source
theorem Filter.inf_principal_neBot_iff {α : Type u_1} {l : Filter α} {s : Set α} :
(l ⊓ principal s).NeBot ↔ ∀ U ∈ l, (U ∩ s).Nonempty
source
theorem Filter.mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} :
s ∈ f ↔ f ⊓ principal s ᶜ = ⊥
source
theorem Filter.notMem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} :
s ∉ f ↔ (f ⊓ principal s ᶜ).NeBot
source
@[deprecated Filter.notMem_iff_inf_principal_compl (since := "2025-05-23")]
theorem Filter.not_mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} :
s ∉ f ↔ (f ⊓ principal s ᶜ).NeBot

Alias of `Filter.notMem_iff_inf_principal_compl`.

source
@[simp]
theorem Filter.disjoint_principal_right {α : Type u_1} {f : Filter α} {s : Set α} :
Disjoint f (principal s) ↔ s ᶜ ∈ f
source
@[simp]
theorem Filter.disjoint_principal_left {α : Type u_1} {f : Filter α} {s : Set α} :
Disjoint (principal s) f ↔ s ᶜ ∈ f
source
@[simp]
theorem Filter.disjoint_principal_principal {α : Type u_1} {s t : Set α} :
Disjoint (principal s) (principal t) ↔ Disjoint s t
source
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`.

source
@[simp]
theorem Filter.disjoint_pure_pure {α : Type u_1} {x y : α} :
Disjoint (pure x) (pure y) ↔ x ≠ y
source
theorem Filter.HasBasis.disjoint_iff_left {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
Disjoint l l' ↔ ∃ (i : ι), p i ∧ (s i)ᶜ ∈ l'
source
theorem Filter.HasBasis.disjoint_iff_right {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
Disjoint l' l ↔ ∃ (i : ι), p i ∧ (s i)ᶜ ∈ l'
source
theorem Filter.le_iff_forall_inf_principal_compl {α : Type u_1} {f g : Filter α} :
f ≤ g ↔ ∀ V ∈ g, f ⊓ principal V ᶜ = ⊥
source
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
source
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
source
theorem Filter.HasBasis.eq_biInf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
l = ⨅ (i : ι), ⨅ (_ : p i), principal (s i)
source
theorem Filter.HasBasis.eq_iInf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {s : ι → Set α} (h : l.HasBasis (fun (x : ι) => True) s) :
l = ⨅ (i : ι), principal (s i)
source
theorem Filter.hasBasis_iInf_principal {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} (h : Directed (fun (x1 x2 : Set α) => x1 ≥ x2) s) [Nonempty ι] :
(⨅ (i : ι), principal (s i)).HasBasis (fun (x : ι) => True) s
source
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
source
theorem Filter.hasBasis_biInf_principal' {α : Type u_1} {ι : Type u_6} {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
source
theorem Filter.HasBasis.map {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β) (hl : l.HasBasis p s) :
(Filter.map f l).HasBasis p fun (i : ι) => f '' s i
source
theorem Filter.HasBasis.comap {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α) (hl : l.HasBasis p s) :
(Filter.comap f l).HasBasis p fun (i : ι) => f ⁻¹' s i
source
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
source
theorem Filter.HasBasis.forall_mem_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) {x : α} :
(∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
source
theorem Filter.HasBasis.biInf_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {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)
source
theorem Filter.HasBasis.biInter_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {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)
source
theorem Filter.HasBasis.ker {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
l.ker = ⋂ (i : ι), ⋂ (_ : p i), s i
source
structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_6} [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.

Instances For

source
structure Filter.HasAntitoneBasis {α : Type u_1} {ι'' : Type u_6} [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.

Instances For

source
theorem Filter.HasAntitoneBasis.map {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι'' → Set α} (hf : l.HasAntitoneBasis s) (m : α → β) :
(map m l).HasAntitoneBasis fun (x : ι'') => m '' s x
source
theorem Filter.HasAntitoneBasis.comap {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι'' → Set α} (hf : l.HasAntitoneBasis s) (m : β → α) :
(comap m l).HasAntitoneBasis fun (x : ι'') => m ⁻¹' s x
source
theorem Filter.HasAntitoneBasis.iInf_principal {α : Type u_1} {ι : Type u_7} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {s : ι → Set α} (hs : Antitone s) :
(⨅ (i : ι), principal (s i)).HasAntitoneBasis s
source
theorem Filter.HasBasis.tendsto_left_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.tendsto_right_iff {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {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
source
theorem Filter.HasBasis.tendsto_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {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
source
theorem Filter.Tendsto.basis_left {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {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
source
theorem Filter.Tendsto.basis_right {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {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
source
theorem Filter.Tendsto.basis_both {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {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)
source
theorem Filter.HasBasis.prod_pprod {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {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
source
theorem Filter.HasBasis.prod {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {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
source
theorem Filter.HasBasis.principal_prod {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (sa : Set α) (h : lb.HasBasis pb sb) :
(principal sa ×ˢ lb).HasBasis pb fun (x : ι') => sa ×ˢ sb x
source
theorem Filter.HasBasis.prod_principal {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (h : la.HasBasis pa sa) (sb : Set β) :
(la ×ˢ principal sb).HasBasis pa fun (x : ι) => sa x ×ˢ sb
source
theorem Filter.HasBasis.top_prod {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (h : lb.HasBasis pb sb) :
(⊤ ×ˢ lb).HasBasis pb fun (x : ι') => Set.univ ×ˢ sb x
source
theorem Filter.HasBasis.prod_top {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (h : la.HasBasis pa sa) :
(la ×ˢ ⊤).HasBasis pa fun (x : ι) => sa x ×ˢ Set.univ
source
theorem Filter.HasBasis.prod_same_index {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {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
source
theorem Filter.HasBasis.prod_same_index_mono {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [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
source
theorem Filter.HasBasis.prod_same_index_anti {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [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
source
theorem Filter.HasBasis.prod_self {α : Type u_1} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (hl : la.HasBasis pa sa) :
(la ×ˢ la).HasBasis pa fun (i : ι) => sa i ×ˢ sa i
source
theorem Filter.mem_prod_self_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} :
s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
source
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
source
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.

source
theorem Filter.HasAntitoneBasis.prod {α : Type u_1} {β : Type u_2} {ι : Type u_6} [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
source
theorem Filter.HasBasis.coprod {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {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
source
theorem Filter.map_sigma_mk_comap {α : Type u_1} {β : Type u_2} {π : α → Type u_6} {π' : β → Type u_7} {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)