Mathlib.Order.Filter.Bases.Basic

FilterBasis structure

(α : Type*)

Full source

/-- 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. -/
structure FilterBasis (α : Type*) where
  /-- Sets of a filter basis. -/
  sets : Set (Set α)
  /-- The set of filter basis sets is nonempty. -/
  nonempty : sets.Nonempty
  /-- The set of filter basis sets is directed downwards. -/
  inter_sets {x y} : x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y

Filter Basis

Informal description

A filter basis on a type $\alpha$ is a nonempty collection of subsets of $\alpha$ such that the intersection of any two elements in this collection contains another element from the collection. This structure is used to generate a filter where a set belongs to the filter if and only if it contains some element from the basis.

FilterBasis.nonempty_sets instance

(B : FilterBasis α) : Nonempty B.sets

Full source

instance FilterBasis.nonempty_sets (B : FilterBasis α) : Nonempty B.sets :=
  B.nonempty.to_subtype

Nonempty Sets in a Filter Basis

Informal description

For any filter basis $B$ on a type $\alpha$, the collection of sets in $B$ is nonempty.

instMembershipSetFilterBasis instance

{α : Type*} : Membership (Set α) (FilterBasis α)

Full source

/-- If `B` is a filter basis on `α`, and `U` a subset of `α` then we can write `U ∈ B` as
on paper. -/
instance {α : Type*} : Membership (Set α) (FilterBasis α) :=
  ⟨fun B U => U ∈ B.sets⟩

Membership Relation for Sets in a Filter Basis

Informal description

For any type $\alpha$, a subset $U$ of $\alpha$ can be considered as an element of a filter basis $B$ on $\alpha$ using the standard membership notation $U \in B$.

FilterBasis.mem_sets theorem

{s : Set α} {B : FilterBasis α} : s ∈ B.sets ↔ s ∈ B

Full source

@[simp] theorem FilterBasis.mem_sets {s : Set α} {B : FilterBasis α} : s ∈ B.setss ∈ B.sets ↔ s ∈ B := Iff.rfl

Membership Equivalence in Filter Basis Sets

Informal description

For any set $s$ of type $\alpha$ and any filter basis $B$ on $\alpha$, the set $s$ is in the collection of sets of $B$ if and only if $s$ is an element of $B$.

instInhabitedFilterBasisNat instance

: Inhabited (FilterBasis ℕ)

Full source

instance : Inhabited (FilterBasis ℕ) :=
  ⟨{  sets := range Ici
      nonempty := ⟨Ici 0, mem_range_self 0⟩
      inter_sets := by
        rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
        exact ⟨Ici (max n m), mem_range_self _, Ici_inter_Ici.symm.subset⟩ }⟩

Filter Basis Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical filter basis structure.

Filter.asBasis definition

(f : Filter α) : FilterBasis α

Full source

/-- View a filter as a filter basis. -/
def Filter.asBasis (f : Filter α) : FilterBasis α :=
  ⟨f.sets, ⟨univ, univ_mem⟩, fun {x y} hx hy => ⟨x ∩ y, inter_mem hx hy, subset_rfl⟩⟩

Filter as a filter basis

Informal description

Given a filter $f$ on a type $\alpha$, the function `Filter.asBasis` constructs a filter basis where the collection of sets is exactly the sets belonging to $f$. The basis is nonempty (since the universal set is in $f$) and closed under finite intersections (since $f$ is closed under finite intersections).

Filter.IsBasis structure

(p : ι → Prop) (s : ι → Set α)

Full source

/-- `IsBasis p s` means the image of `s` bounded by `p` is a filter basis. -/
structure Filter.IsBasis (p : ι → Prop) (s : ι → Set α) : Prop where
  /-- 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

Filter Basis Property

Informal description

Given an indexing type $\iota$, a predicate $p : \iota \to \text{Prop}$, and a map $s : \iota \to \text{Set } \alpha$, the structure `Filter.IsBasis p s` asserts that the collection of sets $\{s(i) \mid p(i)\}$ forms a filter basis on $\alpha$. This means the collection is nonempty and for any two sets $s(i)$ and $s(j)$ in the collection with $p(i)$ and $p(j)$, there exists another set $s(k)$ in the collection with $p(k)$ such that $s(k) \subseteq s(i) \cap s(j)$.

Filter.IsBasis.filterBasis definition

{p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) : FilterBasis α

Full source

/-- Constructs a filter basis from an indexed family of sets satisfying `IsBasis`. -/
protected def filterBasis {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) : FilterBasis α where
  sets := { t | ∃ i, p i ∧ s i = t }
  nonempty :=
    let ⟨i, hi⟩ := h.nonempty
    ⟨s i, ⟨i, hi, rfl⟩⟩
  inter_sets := by
    rintro _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩
    rcases h.inter hi hj with ⟨k, hk, hk'⟩
    exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩

Filter basis construction from indexed family

Informal description

Given an indexing type $\iota$, a predicate $p : \iota \to \text{Prop}$, and a map $s : \iota \to \text{Set } \alpha$, if $h : \text{Filter.IsBasis } p \ s$ holds, then $\text{Filter.IsBasis.filterBasis } h$ constructs a filter basis on $\alpha$ consisting of all sets $s(i)$ for which $p(i)$ is true. Specifically: 1. The collection of sets is $\{s(i) \mid p(i)\}$. 2. The collection is nonempty because there exists at least one $i$ with $p(i)$ (from $h.\text{nonempty}$). 3. For any two sets $s(i)$ and $s(j)$ in the collection (with $p(i)$ and $p(j)$), there exists a set $s(k)$ in the collection (with $p(k)$) such that $s(k) \subseteq s(i) \cap s(j)$ (from $h.\text{inter}$).

Filter.IsBasis.mem_filterBasis_iff theorem

{U : Set α} : U ∈ h.filterBasis ↔ ∃ i, p i ∧ s i = U

Full source

theorem mem_filterBasis_iff {U : Set α} : U ∈ h.filterBasisU ∈ h.filterBasis ↔ ∃ i, p i ∧ s i = U :=
  Iff.rfl

Membership Criterion for Filter Basis Generated by Indexed Family

Informal description

For any subset $U$ of $\alpha$, $U$ belongs to the filter basis generated by $h$ if and only if there exists an index $i$ such that the predicate $p(i)$ holds and the set $s(i)$ equals $U$. In other words: \[ U \in h.\text{filterBasis} \iff \exists i, p(i) \land s(i) = U. \]

FilterBasis.filter definition

(B : FilterBasis α) : Filter α

Full source

/-- The filter associated to a filter basis. -/
protected def filter (B : FilterBasis α) : Filter α where
  sets := { s | ∃ t ∈ B, t ⊆ s }
  univ_sets := B.nonempty.imp fun s s_in => ⟨s_in, s.subset_univ⟩
  sets_of_superset := fun ⟨s, s_in, h⟩ hxy => ⟨s, s_in, Set.Subset.trans h hxy⟩
  inter_sets := fun ⟨_s, s_in, hs⟩ ⟨_t, t_in, ht⟩ =>
    let ⟨u, u_in, u_sub⟩ := B.inter_sets s_in t_in
    ⟨u, u_in, u_sub.trans (inter_subset_inter hs ht)⟩

Filter generated by a filter basis

Informal description

Given a filter basis $ B $ on a type $ \alpha $, the associated filter $ B.\text{filter} $ is defined as the collection of all subsets $ s $ of $ \alpha $ that contain some element $ t $ from $ B $. Formally, $ s \in B.\text{filter} $ if and only if there exists $ t \in B $ such that $ t \subseteq s $. The filter satisfies the following properties: 1. The universal set $ \alpha $ is in $ B.\text{filter} $ because $ B $ is nonempty and any element of $ B $ is a subset of $ \alpha $. 2. If $ s \in B.\text{filter} $ and $ s \subseteq s' $, then $ s' \in B.\text{filter} $. 3. The intersection of any two sets in $ B.\text{filter} $ is also in $ B.\text{filter} $, as the filter basis $ B $ is closed under finite intersections.

FilterBasis.mem_filter_iff theorem

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

Full source

theorem mem_filter_iff (B : FilterBasis α) {U : Set α} : U ∈ B.filterU ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U :=
  Iff.rfl

Membership Criterion for Filter Generated by a Basis

Informal description

Let $B$ be a filter basis on a type $\alpha$. For any subset $U$ of $\alpha$, $U$ belongs to the filter generated by $B$ if and only if there exists a set $s$ in $B$ such that $s$ is a subset of $U$. In other words: \[ U \in B.\text{filter} \iff \exists s \in B, s \subseteq U. \]

FilterBasis.mem_filter_of_mem theorem

(B : FilterBasis α) {U : Set α} : U ∈ B → U ∈ B.filter

Full source

theorem mem_filter_of_mem (B : FilterBasis α) {U : Set α} : U ∈ B → U ∈ B.filter := fun U_in =>
  ⟨U, U_in, Subset.refl _⟩

Membership in Basis Implies Membership in Generated Filter

Informal description

For any filter basis $B$ on a type $\alpha$ and any subset $U$ of $\alpha$, if $U$ belongs to $B$, then $U$ also belongs to the filter generated by $B$.

FilterBasis.generate theorem

(B : FilterBasis α) : generate B.sets = B.filter

Full source

protected theorem generate (B : FilterBasis α) : generate B.sets = B.filter := by
  apply le_antisymm
  · intro U U_in
    rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
    exact GenerateSets.superset (GenerateSets.basic V_in) h
  · rw [le_generate_iff]
    apply mem_filter_of_mem

Equality of Generated Filter and Basis Filter

Informal description

For any filter basis $B$ on a type $\alpha$, the filter generated by the collection of sets in $B$ is equal to the filter associated with $B$.

Filter.IsBasis.filter definition

(h : IsBasis p s) : Filter α

Full source

/-- Constructs a filter from an indexed family of sets satisfying `IsBasis`. -/
protected def filter (h : IsBasis p s) : Filter α :=
  h.filterBasis.filter

Filter generated by a basis

Informal description

Given an indexing type $\iota$, a predicate $p : \iota \to \text{Prop}$, and a map $s : \iota \to \text{Set } \alpha$, if $h : \text{Filter.IsBasis } p \ s$ holds, then $\text{Filter.IsBasis.filter } h$ constructs a filter on $\alpha$ consisting of all subsets $U$ of $\alpha$ that contain some set $s(i)$ for which $p(i)$ is true. In other words, a set $U$ belongs to the filter if and only if there exists an index $i$ such that $p(i)$ holds and $s(i) \subseteq U$.

Filter.IsBasis.mem_filter_iff theorem

(h : IsBasis p s) {U : Set α} : U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U

Full source

protected theorem mem_filter_iff (h : IsBasis p s) {U : Set α} :
    U ∈ h.filterU ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U := by
  simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff,
    exists_exists_and_eq_and]

Membership Criterion for Filter Generated by Basis

Informal description

Let $\alpha$ be a type, $\iota$ an indexing type, $p : \iota \to \text{Prop}$ a predicate, and $s : \iota \to \text{Set } \alpha$ a map of sets. If $h : \text{Filter.IsBasis } p \ s$ holds, then for any subset $U \subseteq \alpha$, we have: \[ U \in h.\text{filter} \iff \exists i \in \iota, p(i) \text{ and } s(i) \subseteq U. \]

Filter.IsBasis.filter_eq_generate theorem

(h : IsBasis p s) : h.filter = generate {U | ∃ i, p i ∧ s i = U}

Full source

theorem filter_eq_generate (h : IsBasis p s) : h.filter = generate { U | ∃ i, p i ∧ s i = U } := by
  rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]

Equality of Generated Filter and Basis Collection Filter

Informal description

Given an indexing type $\iota$, a predicate $p : \iota \to \text{Prop}$, and a map $s : \iota \to \text{Set } \alpha$, if $h : \text{Filter.IsBasis } p \ s$ holds, then the filter generated by $h$ is equal to the filter generated by the collection of sets $\{s(i) \mid p(i)\}$. In other words, $\text{Filter.IsBasis.filter } h = \text{generate } \{U \mid \exists i, p(i) \land s(i) = U\}$.

Filter.HasBasis structure

(l : Filter α) (p : ι → Prop) (s : ι → Set α)

Full source

/-- 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`. -/
structure HasBasis (l : Filter α) (p : ι → Prop) (s : ι → Set α) : Prop where
  /-- A set `t` belongs to a filter `l` iff it includes an element of the basis. -/
  mem_iff' : ∀ t : Set α, t ∈ lt ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

Filter with Basis Condition

Informal description

A filter `l` on a type `α` is said to have a basis consisting of sets `s : ι → Set α` indexed by a predicate `p : ι → Prop` if a set `t` belongs to `l` if and only if there exists an index `i` such that `p i` holds and the set `s i` is a subset of `t`. In other words, the filter `l` is generated by the collection of sets `{s i | p i}` in the sense that a set is in `l` precisely when it contains some `s i` with `p i` true.

Filter.HasBasis.mem_iff theorem

(hl : l.HasBasis p s) : t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

Full source

/-- Definition of `HasBasis` unfolded with implicit set argument. -/
theorem HasBasis.mem_iff (hl : l.HasBasis p s) : t ∈ lt ∈ l ↔ ∃ i, p i ∧ s i ⊆ t :=
  hl.mem_iff' t

Membership Criterion for Filters with Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Then, for any set $t \subseteq \alpha$, we have $t \in l$ if and only if there exists an index $i$ such that $p(i)$ holds and $s_i \subseteq t$.

Filter.hasBasis_iff theorem

: l.HasBasis p s ↔ ∀ t, t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

Full source

theorem hasBasis_iff : l.HasBasis p s ↔ ∀ t, t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t :=
  ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩

Characterization of Filter Basis: $l \text{ has basis } (p, s) \leftrightarrow \forall t, t \in l \leftrightarrow \exists i, p(i) \wedge s(i) \subseteq t$

Informal description

A filter $l$ on a type $\alpha$ has a basis indexed by a predicate $p : \iota \to \text{Prop}$ and sets $s : \iota \to \text{Set } \alpha$ if and only if for every set $t$, $t$ belongs to $l$ precisely when there exists an index $i$ such that $p(i)$ holds and $s(i) \subseteq t$.

Filter.HasBasis.ex_mem theorem

(h : l.HasBasis p s) : ∃ i, p i

Full source

theorem HasBasis.ex_mem (h : l.HasBasis p s) : ∃ i, p i :=
  (h.mem_iff.mp univ_mem).imp fun _ => And.left

Existence of Index in Filter Basis

Informal description

If a filter $l$ on a type $\alpha$ has a basis consisting of sets $s_i$ indexed by a predicate $p$, then there exists an index $i$ such that $p(i)$ holds.

Filter.HasBasis.nonempty theorem

(h : l.HasBasis p s) : Nonempty ι

Full source

protected theorem HasBasis.nonempty (h : l.HasBasis p s) : Nonempty ι :=
  nonempty_of_exists h.ex_mem

Nonemptiness of Index Type for Filter Basis

Informal description

If a filter $l$ on a type $\alpha$ has a basis indexed by a predicate $p : \iota \to \text{Prop}$ and sets $s : \iota \to \text{Set } \alpha$, then the index type $\iota$ is nonempty.

Filter.IsBasis.hasBasis theorem

(h : IsBasis p s) : HasBasis h.filter p s

Full source

protected theorem IsBasis.hasBasis (h : IsBasis p s) : HasBasis h.filter p s :=
  ⟨fun t => by simp only [h.mem_filter_iff, exists_prop]⟩

Filter Generated by Basis Has Basis Property

Informal description

Given an indexing type $\iota$, a predicate $p : \iota \to \text{Prop}$, and a map $s : \iota \to \text{Set } \alpha$, if $h : \text{Filter.IsBasis } p \ s$ holds, then the filter $\text{Filter.IsBasis.filter } h$ has a basis consisting of the sets $s_i$ indexed by $p$. In other words, a set $U$ belongs to the filter generated by the basis if and only if there exists an index $i$ such that $p(i)$ holds and $s(i) \subseteq U$.

Filter.HasBasis.mem_of_superset theorem

(hl : l.HasBasis p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l

Full source

protected theorem HasBasis.mem_of_superset (hl : l.HasBasis p s) (hi : p i) (ht : s i ⊆ t) :
    t ∈ l :=
  hl.mem_iff.2 ⟨i, hi, ht⟩

Superset of Basis Set Belongs to Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. If $p(i)$ holds for some index $i$ and $s_i \subseteq t$, then $t$ belongs to the filter $l$.

Filter.HasBasis.mem_of_mem theorem

(hl : l.HasBasis p s) (hi : p i) : s i ∈ l

Full source

theorem HasBasis.mem_of_mem (hl : l.HasBasis p s) (hi : p i) : s i ∈ l :=
  hl.mem_of_superset hi Subset.rfl

Basis Set Belongs to Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. If $p(i)$ holds for some index $i$, then the set $s_i$ belongs to the filter $l$.

Filter.HasBasis.index definition

(h : l.HasBasis p s) (t : Set α) (ht : t ∈ l) : { i : ι // p i }

Full source

/-- Index of a basis set such that `s i ⊆ t` as an element of `Subtype p`. -/
noncomputable def HasBasis.index (h : l.HasBasis p s) (t : Set α) (ht : t ∈ l) : { i : ι // p i } :=
  ⟨(h.mem_iff.1 ht).choose, (h.mem_iff.1 ht).choose_spec.1⟩

Index of basis set in filter

Informal description

Given a filter `l` on a type `α` with a basis consisting of sets `s : ι → Set α` indexed by a predicate `p : ι → Prop`, and given a set `t ∈ l`, the function returns an index `i` such that `p i` holds and `s i ⊆ t`. This index is packaged as a term of the subtype `{i : ι // p i}`.

Filter.HasBasis.property_index theorem

(h : l.HasBasis p s) (ht : t ∈ l) : p (h.index t ht)

Full source

theorem HasBasis.property_index (h : l.HasBasis p s) (ht : t ∈ l) : p (h.index t ht) :=
  (h.index t ht).2

Predicate Holds for Index of Basis Set in Filter

Informal description

Given a filter $l$ on a type $\alpha$ with a basis consisting of sets $s : \iota \to \text{Set } \alpha$ indexed by a predicate $p : \iota \to \text{Prop}$, and given a set $t \in l$, the predicate $p$ holds for the index $h.\text{index}(t, ht)$, where $ht$ is a proof that $t \in l$.

Filter.HasBasis.set_index_mem theorem

(h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ∈ l

Full source

theorem HasBasis.set_index_mem (h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ∈ l :=
  h.mem_of_mem <| h.property_index _

Basis Set Membership in Filter via Index

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any set $t \in l$, the basis set $s_{i_t}$ corresponding to the index $i_t = h.\text{index}(t, ht)$ belongs to the filter $l$.

Filter.HasBasis.set_index_subset theorem

(h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ⊆ t

Full source

theorem HasBasis.set_index_subset (h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ⊆ t :=
  (h.mem_iff.1 ht).choose_spec.2

Basis Set Subset Property in Filters

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). For any set $t \in l$, the basis set $s_{i_t}$ corresponding to the index $i_t = h.\text{index}(t, ht)$ is a subset of $t$, i.e., $s_{i_t} \subseteq t$.

Filter.HasBasis.isBasis theorem

(h : l.HasBasis p s) : IsBasis p s

Full source

theorem HasBasis.isBasis (h : l.HasBasis p s) : IsBasis p s where
  nonempty := h.ex_mem
  inter hi hj := by
    simpa only [h.mem_iff] using inter_mem (h.mem_of_mem hi) (h.mem_of_mem hj)

Filter with Basis Forms Filter Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. Then the collection $\{s_i \mid p(i)\}$ forms a filter basis, meaning it is nonempty and for any two sets $s_i$ and $s_j$ in the collection, there exists a set $s_k$ in the collection such that $s_k \subseteq s_i \cap s_j$.

Filter.HasBasis.filter_eq theorem

(h : l.HasBasis p s) : h.isBasis.filter = l

Full source

theorem HasBasis.filter_eq (h : l.HasBasis p s) : h.isBasis.filter = l := by
  ext U
  simp [h.mem_iff, IsBasis.mem_filter_iff]

Filter Equality for Basis-Generated Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. Then the filter generated by this basis is equal to $l$ itself, i.e., $h.\text{isBasis}.\text{filter} = l$.

FilterBasis.hasBasis theorem

(B : FilterBasis α) : HasBasis B.filter (fun s : Set α => s ∈ B) id

Full source

protected theorem _root_.FilterBasis.hasBasis (B : FilterBasis α) :
    HasBasis B.filter (fun s : Set α => s ∈ B) id :=
  ⟨fun _ => B.mem_filter_iff⟩

Filter Generated by Basis Has Basis Condition

Informal description

For any filter basis $B$ on a type $\alpha$, the generated filter $B.\text{filter}$ has a basis consisting of the sets in $B$ themselves. Specifically, a set $U$ belongs to $B.\text{filter}$ if and only if there exists a set $s \in B$ such that $s \subseteq U$. In other words, the filter basis condition holds with the predicate $p(s) := s \in B$ and the identity mapping $s \mapsto s$: \[ B.\text{filter} \text{ has basis } \{s \mid s \in B\}. \]

Filter.HasBasis.to_hasBasis' theorem

 (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'

Full source

theorem HasBasis.to_hasBasis' (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' := by
  refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩
  rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩
  rcases h i hi with ⟨i', hi', hs's⟩
  exact ⟨i', hi', hs's.trans ht⟩

Filter Basis Transformation via Subset Inclusion

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $(p, s)$, where $p : \iota \to \text{Prop}$ and $s : \iota \to \text{Set} \alpha$. Suppose that for every index $i$ with $p(i)$, there exists an index $i'$ such that $p'(i')$ holds and $s'(i') \subseteq s(i)$. Furthermore, assume that for every $i'$ with $p'(i')$, the set $s'(i')$ belongs to $l$. Then $l$ also has the basis $(p', s')$.

Filter.HasBasis.to_hasBasis theorem

 (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'

Full source

theorem HasBasis.to_hasBasis (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' :=
  hl.to_hasBasis' h fun i' hi' =>
    let ⟨i, hi, hss'⟩ := h' i' hi'
    hl.mem_iff.2 ⟨i, hi, hss'⟩

Filter Basis Transformation via Mutual Subset Inclusion

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $(p, s)$, where $p : \iota \to \text{Prop}$ and $s : \iota \to \text{Set} \alpha$. Suppose that for every index $i$ with $p(i)$, there exists an index $i'$ such that $p'(i')$ holds and $s'(i') \subseteq s(i)$. Furthermore, assume that for every $i'$ with $p'(i')$, there exists an index $i$ such that $p(i)$ holds and $s(i) \subseteq s'(i')$. Then $l$ also has the basis $(p', s')$.

Filter.HasBasis.congr theorem

(hl : l.HasBasis p s) {p' s'} (hp : ∀ i, p i ↔ p' i) (hs : ∀ i, p i → s i = s' i) : l.HasBasis p' s'

Full source

protected lemma HasBasis.congr (hl : l.HasBasis p s) {p' s'} (hp : ∀ i, p i ↔ p' i)
    (hs : ∀ i, p i → s i = s' i) : l.HasBasis p' s' :=
  ⟨fun t ↦ by simp only [hl.mem_iff, ← hp]; exact exists_congr fun i ↦
    and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl⟩

Equivalence of Filter Bases under Predicate and Set Equality

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Suppose $p'$ and $s'$ are another predicate and family of sets such that for every index $i$, $p(i)$ holds if and only if $p'(i)$ holds, and whenever $p(i)$ holds, $s_i = s'_i$. Then $l$ also has the basis $(p', s')$.

Filter.HasBasis.to_subset theorem

 (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

Full source

theorem HasBasis.to_subset (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 :=
  hl.to_hasBasis' (fun i hi => ⟨i, hi, h i hi⟩) ht

Filter Basis Transformation via Subset Inclusion

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $(p, s)$, where $p : \iota \to \text{Prop}$ and $s : \iota \to \text{Set} \alpha$. Suppose that for every index $i$ with $p(i)$, the set $t_i$ is a subset of $s_i$ and $t_i$ belongs to $l$. Then $l$ also has the basis $(p, t)$.

Filter.HasBasis.eventually_iff theorem

(hl : l.HasBasis p s) {q : α → Prop} : (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x

Full source

theorem HasBasis.eventually_iff (hl : l.HasBasis p s) {q : α → Prop} :
    (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x := by simpa using hl.mem_iff

Eventual Property Criterion for Filters with Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Then, for any predicate $q : \alpha \to \text{Prop}$, the following are equivalent: 1. The predicate $q$ holds eventually in $l$ (i.e., $\forall^l x, q(x)$). 2. There exists an index $i$ such that $p(i)$ holds and for all $x \in s_i$, $q(x)$ holds. In other words, $q$ holds eventually in $l$ if and only if there exists a basis set $s_i$ (with $p(i)$ true) on which $q$ holds uniformly.

Filter.HasBasis.frequently_iff theorem

(hl : l.HasBasis p s) {q : α → Prop} : (∃ᶠ x in l, q x) ↔ ∀ i, p i → ∃ x ∈ s i, q x

Full source

theorem HasBasis.frequently_iff (hl : l.HasBasis p s) {q : α → Prop} :
    (∃ᶠ x in l, q x) ↔ ∀ i, p i → ∃ x ∈ s i, q x := by
  simp only [Filter.Frequently, hl.eventually_iff]; push_neg; rfl

Frequent Property Criterion for Filters with Basis: $\exists^l x, q(x) \leftrightarrow \forall i, p(i) \to \exists x \in s_i, q(x)$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Then, for any predicate $q : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $q$ holds frequently in $l$ (i.e., $\exists^l x, q(x)$). 2. For every index $i$ such that $p(i)$ holds, there exists an element $x \in s_i$ for which $q(x)$ holds. In other words, $q$ holds frequently in $l$ if and only if for every basis set $s_i$ (with $p(i)$ true), there exists some $x \in s_i$ satisfying $q(x)$.

Filter.HasBasis.exists_iff theorem

 (hl : l.HasBasis p s) {P : Set α → Prop} (mono : ∀ ⦃s t⦄, s ⊆ t → P t → P s) : (∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i)

Full source

theorem HasBasis.exists_iff (hl : l.HasBasis p s) {P : Set α → Prop}
    (mono : ∀ ⦃s t⦄, s ⊆ t → P t → P s) : (∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i) :=
  ⟨fun ⟨_s, hs, hP⟩ =>
    let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
    ⟨i, hi, mono his hP⟩,
    fun ⟨i, hi, hP⟩ => ⟨s i, hl.mem_of_mem hi, hP⟩⟩

Existence Criterion for Antitone Properties in Filters with Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). For any property $P$ on sets that is antitone (i.e., if $s \subseteq t$ and $P(t)$ holds, then $P(s)$ holds), the following are equivalent: 1. There exists a set $s \in l$ such that $P(s)$ holds. 2. There exists an index $i$ such that $p(i)$ holds and $P(s_i)$ holds.

Filter.HasBasis.forall_iff theorem

 (hl : l.HasBasis p s) {P : Set α → Prop} (mono : ∀ ⦃s t⦄, s ⊆ t → P s → P t) : (∀ s ∈ l, P s) ↔ ∀ i, p i → P (s i)

Full source

theorem HasBasis.forall_iff (hl : l.HasBasis p s) {P : Set α → Prop}
    (mono : ∀ ⦃s t⦄, s ⊆ t → P s → P t) : (∀ s ∈ l, P s) ↔ ∀ i, p i → P (s i) :=
  ⟨fun H i hi => H (s i) <| hl.mem_of_mem hi, fun H _s hs =>
    let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
    mono his (H i hi)⟩

Universal Property Criterion for Filters with Basis: $\forall s \in l, P(s) \leftrightarrow \forall i, p(i) \to P(s_i)$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any property $P$ on sets that is monotone with respect to inclusion (i.e., if $s \subseteq t$ and $P(s)$ holds, then $P(t)$ holds), the following are equivalent: 1. For every set $s$ in the filter $l$, the property $P(s)$ holds. 2. For every index $i$ such that $p(i)$ holds, the property $P(s_i)$ holds.

Filter.HasBasis.neBot_iff theorem

(hl : l.HasBasis p s) : NeBot l ↔ ∀ {i}, p i → (s i).Nonempty

Full source

protected theorem HasBasis.neBot_iff (hl : l.HasBasis p s) :
    NeBotNeBot l ↔ ∀ {i}, p i → (s i).Nonempty :=
  forall_mem_nonempty_iff_neBot.symm.trans <| hl.forall_iff fun _ _ => Nonempty.mono

Non-triviality Criterion for Filters with Basis: $\text{NeBot } l \leftrightarrow \forall i, p(i) \to s_i \neq \emptyset$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. Then $l$ is non-trivial (i.e., $\text{NeBot } l$) if and only if for every index $i$ such that $p(i)$ holds, the set $s_i$ is nonempty.

Filter.basis_sets theorem

(l : Filter α) : l.HasBasis (fun s : Set α => s ∈ l) id

Full source

theorem basis_sets (l : Filter α) : l.HasBasis (fun s : Set α => s ∈ l) id :=
  ⟨fun _ => exists_mem_subset_iff.symm⟩

Filter Basis from All Sets in a Filter

Informal description

For any filter $l$ on a type $\alpha$, the collection of all sets in $l$ forms a basis for $l$. That is, a set $t$ belongs to $l$ if and only if there exists a set $s \in l$ such that $s \subseteq t$.

Filter.asBasis_filter theorem

(f : Filter α) : f.asBasis.filter = f

Full source

theorem asBasis_filter (f : Filter α) : f.asBasis.filter = f :=
  Filter.ext fun _ => exists_mem_subset_iff

Filter Generated by Its Own Basis Equals Itself

Informal description

For any filter $f$ on a type $\alpha$, the filter generated by the basis consisting of all sets in $f$ is equal to $f$ itself.

Filter.hasBasis_self theorem

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

Full source

theorem hasBasis_self {l : Filter α} {P : Set α → Prop} :
    HasBasisHasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t := by
  simp only [hasBasis_iff, id, and_assoc]
  exact forall_congr' fun s =>
    ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

Characterization of Filter Basis via Predicate $P$

Informal description

A filter $l$ on a type $\alpha$ has a basis consisting of sets $s$ in $l$ that satisfy a predicate $P$ (i.e., $l$ has the basis $\{s \in l \mid P(s)\}$) if and only if for every set $t \in l$, there exists a set $r \in l$ such that $P(r)$ holds and $r \subseteq t$.

Filter.HasBasis.comp_surjective theorem

(h : l.HasBasis p s) {g : ι' → ι} (hg : Function.Surjective g) : l.HasBasis (p ∘ g) (s ∘ g)

Full source

theorem HasBasis.comp_surjective (h : l.HasBasis p s) {g : ι' → ι} (hg : Function.Surjective g) :
    l.HasBasis (p ∘ g) (s ∘ g) :=
  ⟨fun _ => h.mem_iff.trans hg.exists⟩

Surjective Precomposition Preserves Filter Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). If $g : \iota' \to \iota$ is a surjective function, then $l$ also has a basis consisting of sets $s_{g(i')}$ indexed by the predicate $p \circ g$ (i.e., $l$ has the basis $(p \circ g, s \circ g)$).

Filter.HasBasis.comp_equiv theorem

(h : l.HasBasis p s) (e : ι' ≃ ι) : l.HasBasis (p ∘ e) (s ∘ e)

Full source

theorem HasBasis.comp_equiv (h : l.HasBasis p s) (e : ι' ≃ ι) : l.HasBasis (p ∘ e) (s ∘ e) :=
  h.comp_surjective e.surjective

Equivalence of Index Types Preserves Filter Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). If $e : \iota' \simeq \iota$ is an equivalence between index types, then $l$ also has a basis consisting of sets $s_{e(i')}$ indexed by the predicate $p \circ e$ (i.e., $l$ has the basis $(p \circ e, s \circ e)$).

Filter.HasBasis.to_image_id' theorem

(h : l.HasBasis p s) : l.HasBasis (fun t ↦ ∃ i, p i ∧ s i = t) id

Full source

theorem HasBasis.to_image_id' (h : l.HasBasis p s) : l.HasBasis (fun t ↦ ∃ i, p i ∧ s i = t) id :=
  ⟨fun _ ↦ by simp [h.mem_iff]⟩

Filter Basis Characterization via Image of Indexed Sets

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Then $l$ also has a basis consisting of the identity function on sets, where the predicate is given by $\exists i, p i \land s i = t$ for each set $t \subseteq \alpha$. In other words, $l$ can be described as the filter generated by the sets $s_i$ themselves (rather than their indices), where a set $t$ is in the basis if and only if it equals some $s_i$ with $p i$ true.

Filter.HasBasis.to_image_id theorem

{ι : Type*} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l.HasBasis (· ∈ s '' {i | p i}) id

Full source

theorem HasBasis.to_image_id {ι : Type*} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
    l.HasBasis (· ∈ s '' {i | p i}) id :=
  h.to_image_id'

Filter Basis Characterization via Image of Predicate-Satisfying Indices

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). Then $l$ also has a basis consisting of the identity function on sets, where the predicate is given by membership in the image of $\{i \mid p i\}$ under $s$ (i.e., $t$ is in the basis if and only if $t \in s''\{i \mid p i\}$). In other words, $l$ can be described as the filter generated by the sets $s_i$ themselves (rather than their indices), where a set $t$ is in the basis if and only if it equals some $s_i$ with $p i$ true.

Filter.HasBasis.restrict theorem

 (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

Full source

/-- 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 HasBasis.restrict (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 := by
  refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
  rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
  rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
  exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩

Filter Basis Restriction Theorem

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $\{s_i \mid p_i\}$ where $p : \iota \to \text{Prop}$ and $s : \iota \to \text{Set } \alpha$. Suppose that for every $i$ with $p_i$ true, there exists $j$ such that $p_j$ and $q_j$ are true and $s_j \subseteq s_i$. Then $\{s_j \mid p_j \land q_j\}$ is also a basis for $l$.

Filter.HasBasis.restrict_subset theorem

(h : l.HasBasis p s) {V : Set α} (hV : V ∈ l) : l.HasBasis (fun i => p i ∧ s i ⊆ V) s

Full source

/-- 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 HasBasis.restrict_subset (h : l.HasBasis p s) {V : Set α} (hV : V ∈ l) :
    l.HasBasis (fun i => p i ∧ s i ⊆ V) s :=
  h.restrict fun _i hi => (h.mem_iff.1 (inter_mem hV (h.mem_of_mem hi))).imp fun _j hj =>
    ⟨hj.1, subset_inter_iff.1 hj.2⟩

Restriction of Filter Basis to a Subset

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $\{s_i \mid p_i\}$ where $p : \iota \to \text{Prop}$ and $s : \iota \to \text{Set } \alpha$. If $V$ is a set in $l$, then the collection $\{s_i \mid p_i \land s_i \subseteq V\}$ also forms a basis for $l$.

Filter.HasBasis.hasBasis_self_subset theorem

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

Full source

theorem HasBasis.hasBasis_self_subset {p : Set α → Prop} (h : l.HasBasis (fun s => s ∈ ls ∈ l ∧ p s) id)
    {V : Set α} (hV : V ∈ l) : l.HasBasis (fun s => s ∈ ls ∈ l ∧ p s ∧ s ⊆ V) id := by
  simpa only [and_assoc] using h.restrict_subset hV

Filter Basis Restriction to Subsets of a Given Set

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of all sets $s \in l$ satisfying a predicate $p : \text{Set } \alpha \to \text{Prop}$. For any set $V \in l$, the collection of all sets $s \in l$ that satisfy $p(s)$ and are subsets of $V$ also forms a basis for $l$.

Filter.HasBasis.ge_iff theorem

(hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l

Full source

theorem HasBasis.ge_iff (hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
  ⟨fun h _i' hi' => h <| hl'.mem_of_mem hi', fun h _s hs =>
    let ⟨_i', hi', hs⟩ := hl'.mem_iff.1 hs
    mem_of_superset (h _ hi') hs⟩

Filter Fineness Criterion via Basis Membership

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$, and suppose $l'$ has a basis consisting of sets $s'_{i'}$ indexed by a predicate $p'$. Then $l$ is finer than $l'$ (i.e., $l \leq l'$) if and only if for every index $i'$ such that $p'(i')$ holds, the set $s'_{i'}$ belongs to $l$.

Filter.HasBasis.le_iff theorem

(hl : l.HasBasis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t

Full source

theorem HasBasis.le_iff (hl : l.HasBasis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t := by
  simp only [le_def, hl.mem_iff]

Filter Fineness Criterion via Basis Elements

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$, and suppose $l$ has a basis consisting of sets $s_i$ indexed by a predicate $p$. Then $l$ is finer than $l'$ (i.e., $l \leq l'$) if and only if for every set $t \in l'$, there exists an index $i$ such that $p(i)$ holds and $s_i \subseteq t$.

Filter.HasBasis.le_basis_iff theorem

(hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Full source

theorem HasBasis.le_basis_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    l ≤ l' ↔ ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i' := by
  simp only [hl'.ge_iff, hl.mem_iff]

Filter Fineness Criterion via Basis Elements: $l \leq l'$ iff $\forall i', p'(i') \to \exists i, p(i) \land s_i \subseteq s'_{i'}$

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$, where $l$ has a basis consisting of sets $s_i$ indexed by a predicate $p$, and $l'$ has a basis consisting of sets $s'_{i'}$ indexed by a predicate $p'$. Then $l$ is finer than $l'$ (i.e., $l \leq l'$) if and only if for every index $i'$ such that $p'(i')$ holds, there exists an index $i$ such that $p(i)$ holds and $s_i \subseteq s'_{i'}$.

Filter.HasBasis.ext theorem

 (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'

Full source

theorem HasBasis.ext (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' := by
  apply le_antisymm
  · rw [hl.le_basis_iff hl']
    simpa using h'
  · rw [hl'.le_basis_iff hl]
    simpa using h

Filter Equality via Basis Interchangeability

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$, where $l$ has a basis consisting of sets $s_i$ indexed by a predicate $p$, and $l'$ has a basis consisting of sets $s'_{i'}$ indexed by a predicate $p'$. If for every index $i$ with $p(i)$ there exists an index $i'$ with $p'(i')$ and $s'_{i'} \subseteq s_i$, and conversely for every index $i'$ with $p'(i')$ there exists an index $i$ with $p(i)$ and $s_i \subseteq s'_{i'}$, then $l = l'$.

Filter.HasBasis.inf' theorem

 (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
  (l ⊓ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2

Full source

theorem HasBasis.inf' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    (l ⊓ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2 :=
  ⟨by
    intro t
    constructor
    · simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
      rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩
      exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩
    · rintro ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩
      exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H⟩

Basis Characterization for Infimum of Two Filters

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, $s' : \iota' \to \text{Set } \alpha$. Then the infimum filter $l \sqcap l'$ has a basis consisting of sets $s(i_1) \cap s'(i_2)$ indexed by pairs $(i_1, i_2) \in \iota \times \iota'$ (represented as `PProd ι ι'`) where both $p(i_1)$ and $p'(i_2)$ hold.

Filter.HasBasis.inf theorem

 {ι ι' : Type*} {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

Full source

theorem HasBasis.inf {ι ι' : Type*} {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 :=
  (hl.inf' hl').comp_equiv Equiv.pprodEquivProd.symm

Basis Characterization for Infimum of Two Filters via Cartesian Product

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, $s' : \iota' \to \text{Set } \alpha$. Then the infimum filter $l \sqcap l'$ has a basis consisting of sets $s(i_1) \cap s'(i_2)$ indexed by pairs $(i_1, i_2) \in \iota \times \iota'$ where both $p(i_1)$ and $p'(i_2)$ hold.

Filter.hasBasis_iInf_of_directed' theorem

 {ι : Type*} {ι' : ι → Sort _} [Nonempty ι] {l : ι → Filter α} (s : ∀ i, ι' i → Set α) (p : ∀ i, ι' i → Prop)
  (hl : ∀ i, (l i).HasBasis (p i) (s i)) (h : Directed (· ≥ ·) l) :
  (⨅ i, l i).HasBasis (fun ii' : Σ i, ι' i => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Full source

theorem hasBasis_iInf_of_directed' {ι : Type*} {ι' : ι → Sort _} [Nonempty ι] {l : ι → Filter α}
    (s : ∀ i, ι' i → Set α) (p : ∀ i, ι' i → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i))
    (h : Directed (· ≥ ·) l) :
    (⨅ i, l i).HasBasis (fun ii' : Σi, ι' i => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2 := by
  refine ⟨fun t => ?_⟩
  rw [mem_iInf_of_directed h, Sigma.exists]
  exact exists_congr fun i => (hl i).mem_iff

Basis characterization for infimum of directed family of filters

Informal description

Let $\{l_i\}_{i \in \iota}$ be a nonempty directed family of filters on a type $\alpha$ with respect to reverse inclusion (i.e., for any $i,j \in \iota$, there exists $k \in \iota$ such that $l_k \subseteq l_i$ and $l_k \subseteq l_j$). Suppose each filter $l_i$ has a basis consisting of sets $s_i(j)$ indexed by a predicate $p_i(j)$ where $j \in \iota'_i$. Then the infimum filter $\bigsqcap_{i} l_i$ has a basis consisting of all sets $s_i(j)$ where $(i,j)$ ranges over all pairs in the sigma type $\Sigma (i : \iota), \iota'_i$ with $p_i(j)$ true.

Filter.hasBasis_iInf_of_directed theorem

 {ι : Type*} {ι' : Sort _} [Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop)
  (hl : ∀ i, (l i).HasBasis (p i) (s i)) (h : Directed (· ≥ ·) l) :
  (⨅ i, l i).HasBasis (fun ii' : ι × ι' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Full source

theorem hasBasis_iInf_of_directed {ι : Type*} {ι' : Sort _} [Nonempty ι] {l : ι → Filter α}
    (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i))
    (h : Directed (· ≥ ·) l) :
    (⨅ i, l i).HasBasis (fun ii' : ι × ι' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2 := by
  refine ⟨fun t => ?_⟩
  rw [mem_iInf_of_directed h, Prod.exists]
  exact exists_congr fun i => (hl i).mem_iff

Basis Characterization for Infimum of Directed Family of Filters

Informal description

Let $\{l_i\}_{i \in \iota}$ be a nonempty family of filters on a type $\alpha$, indexed by a type $\iota$, and let $s_i : \iota' \to \text{Set } \alpha$ and $p_i : \iota' \to \text{Prop}$ be families of sets and predicates for each $i \in \iota$. Suppose that for each $i$, the filter $l_i$ has a basis given by $(p_i, s_i)$, and that the family $\{l_i\}$ is directed with respect to the reverse inclusion order $\geq$. Then the infimum filter $\bigsqcap_i l_i$ has a basis consisting of sets $s_{i}(j)$ indexed by pairs $(i,j) \in \iota \times \iota'$ where $p_i(j)$ holds.

Filter.hasBasis_biInf_of_directed' theorem

 {ι : Type*} {ι' : ι → Sort _} {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'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Full source

theorem hasBasis_biInf_of_directed' {ι : Type*} {ι' : ι → Sort _} {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'.1 ∈ domii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' =>
      s ii'.1 ii'.2 := by
  refine ⟨fun t => ?_⟩
  rw [mem_biInf_of_directed h hdom, Sigma.exists]
  refine exists_congr fun i => ⟨?_, ?_⟩
  · rintro ⟨hi, hti⟩
    rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩
    exact ⟨b, ⟨hi, hb⟩, hbt⟩
  · rintro ⟨b, ⟨hi, hb⟩, hibt⟩
    exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩

Basis Characterization for Infimum of Directed Family of Filters over a Nonempty Subset

Informal description

Let $\{l_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, indexed by a nonempty subset $\text{dom} \subseteq \iota$. For each $i \in \text{dom}$, let $l_i$ have a basis consisting of sets $s_i(j)$ indexed by a predicate $p_i(j)$ where $j \in \iota'_i$. Suppose the family $\{l_i\}_{i \in \text{dom}}$ is directed with respect to reverse inclusion (i.e., for any $i, i' \in \text{dom}$, there exists $k \in \text{dom}$ such that $l_k \subseteq l_i$ and $l_k \subseteq l_{i'}$). Then the infimum filter $\bigsqcap_{i \in \text{dom}} l_i$ has a basis consisting of all sets $s_i(j)$ where $(i,j)$ ranges over all pairs in the sigma type $\Sigma (i : \iota), \iota'_i$ with $i \in \text{dom}$ and $p_i(j)$ true.

Filter.hasBasis_biInf_of_directed theorem

 {ι : Type*} {ι' : Sort _} {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

Full source

theorem hasBasis_biInf_of_directed {ι : Type*} {ι' : Sort _} {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 ∈ domii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' =>
      s ii'.1 ii'.2 := by
  refine ⟨fun t => ?_⟩
  rw [mem_biInf_of_directed h hdom, Prod.exists]
  refine exists_congr fun i => ⟨?_, ?_⟩
  · rintro ⟨hi, hti⟩
    rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩
    exact ⟨b, ⟨hi, hb⟩, hbt⟩
  · rintro ⟨b, ⟨hi, hb⟩, hibt⟩
    exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩

Basis Characterization for Infimum of Directed Family of Filters over a Nonempty Domain

Informal description

Let $\{l_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, indexed by a type $\iota$, and let $s_i : \iota' \to \text{Set } \alpha$ and $p_i : \iota' \to \text{Prop}$ be families of sets and predicates for each $i \in \iota$. Suppose that for each $i$ in a nonempty subset $\text{dom} \subseteq \iota$, the filter $l_i$ has a basis given by $(p_i, s_i)$, and that the family $\{l_i\}_{i \in \text{dom}}$ is directed with respect to the reverse inclusion order $\geq$. Then the infimum filter $\bigsqcap_{i \in \text{dom}} l_i$ has a basis consisting of sets $s_{i}(j)$ indexed by pairs $(i,j) \in \iota \times \iota'$ where $i \in \text{dom}$ and $p_i(j)$ holds.

Filter.hasBasis_principal theorem

(t : Set α) : (𝓟 t).HasBasis (fun _ : Unit => True) fun _ => t

Full source

theorem hasBasis_principal (t : Set α) : (𝓟 t).HasBasis (fun _ : Unit => True) fun _ => t :=
  ⟨fun U => by simp⟩

Principal Filter Basis: $\mathfrak{p}(t)$ has basis $\{t\}$

Informal description

For any set $t$ in a type $\alpha$, the principal filter $\mathfrak{p}(t)$ has a basis consisting of the single set $t$, indexed by the trivial condition (always true). That is, a set belongs to $\mathfrak{p}(t)$ if and only if it contains $t$.

Filter.hasBasis_pure theorem

(x : α) : (pure x : Filter α).HasBasis (fun _ : Unit => True) fun _ => { x }

Full source

theorem hasBasis_pure (x : α) :
    (pure x : Filter α).HasBasis (fun _ : Unit => True) fun _ => {x} := by
  simp only [← principal_singleton, hasBasis_principal]

Pure Filter Basis: $\text{pure } x$ has basis $\{x\}$

Informal description

For any element $x$ in a type $\alpha$, the pure filter $\text{pure } x$ (which consists of all sets containing $x$) has a basis consisting of the singleton set $\{x\}$, indexed by the trivial condition (always true).

Filter.HasBasis.sup' theorem

 (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
  (l ⊔ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2

Full source

theorem HasBasis.sup' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    (l ⊔ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2 :=
  ⟨by
    intro t
    simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]
    simp only [and_assoc, and_left_comm]⟩

Supremum of Filters with Given Bases Has Union Basis

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, and $s' : \iota' \to \text{Set } \alpha$. Then the supremum filter $l \sqcup l'$ has a basis indexed by pairs $(i,j) \in \iota \times \iota'$ (using the type `PProd` for dependent pairs) where $p(i)$ and $p'(j)$ both hold, and the corresponding basis sets are the unions $s(i) \cup s'(j)$. In other words, a set belongs to $l \sqcup l'$ if and only if it contains a union $s(i) \cup s'(j)$ for some indices $i$ and $j$ satisfying $p(i)$ and $p'(j)$ respectively.

Filter.HasBasis.sup theorem

 {ι ι' : Type*} {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

Full source

theorem HasBasis.sup {ι ι' : Type*} {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 :=
  (hl.sup' hl').comp_equiv Equiv.pprodEquivProd.symm

Supremum of Filters with Cartesian Product Basis: $l \sqcup l'$ has basis $\{s_i \cup s'_j\}_{p(i) \land p'(j)}$

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, and $s' : \iota' \to \text{Set } \alpha$. Then the supremum filter $l \sqcup l'$ has a basis indexed by pairs $(i,j) \in \iota \times \iota'$ where $p(i)$ and $p'(j)$ both hold, and the corresponding basis sets are the unions $s(i) \cup s'(j)$. In other words, a set belongs to $l \sqcup l'$ if and only if it contains a union $s(i) \cup s'(j)$ for some indices $i$ and $j$ satisfying $p(i)$ and $p'(j)$ respectively.

Filter.hasBasis_iSup theorem

 {ι : Sort*} {ι' : ι → Type*} {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)

Full source

theorem hasBasis_iSup {ι : Sort*} {ι' : ι → Type*} {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) :=
  hasBasis_iff.mpr fun t => by
    simp only [hasBasis_iff, (hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
      mem_iSup]

Basis Characterization for Supremum of Filters: $\bigsqcup_i l_i$ has basis $\bigcup_i s_i(f(i))$ for $f$ with $p_i(f(i))$ for all $i$

Informal description

Let $\{l_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, where for each $i \in \iota$, the filter $l_i$ has a basis consisting of sets $\{s_i(j)\}_{j \in \iota'_i}$ indexed by a predicate $p_i : \iota'_i \to \text{Prop}$. Then the supremum filter $\bigsqcup_{i \in \iota} l_i$ has a basis consisting of sets $\bigcup_{i \in \iota} s_i(f(i))$ indexed by functions $f \in \prod_{i \in \iota} \iota'_i$ satisfying $\forall i, p_i(f(i))$.

Filter.HasBasis.sup_principal theorem

(hl : l.HasBasis p s) (t : Set α) : (l ⊔ 𝓟 t).HasBasis p fun i => s i ∪ t

Full source

theorem HasBasis.sup_principal (hl : l.HasBasis p s) (t : Set α) :
    (l ⊔ 𝓟 t).HasBasis p fun i => s i ∪ t :=
  ⟨fun u => by
    simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, exists_prop, and_true,
      Unique.exists_iff]⟩

Basis for Supremum of Filter with Principal Filter: $l \sqcup \mathfrak{P}(t)$ has basis $\{s_i \cup t\}_{p(i)}$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $\{s_i\}_{i \in \iota}$ indexed by a predicate $p : \iota \to \text{Prop}$. For any subset $t \subseteq \alpha$, the supremum filter $l \sqcup \mathfrak{P}(t)$ has a basis consisting of the sets $s_i \cup t$ indexed by the same predicate $p$. Here, $\mathfrak{P}(t)$ denotes the principal filter generated by $t$, and $\sqcup$ denotes the supremum (join) of two filters.

Filter.HasBasis.sup_pure theorem

(hl : l.HasBasis p s) (x : α) : (l ⊔ pure x).HasBasis p fun i => s i ∪ { x }

Full source

theorem HasBasis.sup_pure (hl : l.HasBasis p s) (x : α) :
    (l ⊔ pure x).HasBasis p fun i => s i ∪ {x} := by
  simp only [← principal_singleton, hl.sup_principal]

Basis for Supremum of Filter with Principal Filter of Singleton: $l \sqcup \text{pure }x$ has basis $\{s_i \cup \{x\}\}_{p(i)}$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $\{s_i\}_{i \in \iota}$ indexed by a predicate $p : \iota \to \text{Prop}$. For any element $x \in \alpha$, the supremum filter $l \sqcup \text{pure }x$ has a basis consisting of the sets $s_i \cup \{x\}$ indexed by the same predicate $p$. Here, $\text{pure }x$ denotes the principal filter generated by the singleton $\{x\}$, and $\sqcup$ denotes the supremum (join) of two filters.

Filter.HasBasis.inf_principal theorem

(hl : l.HasBasis p s) (s' : Set α) : (l ⊓ 𝓟 s').HasBasis p fun i => s i ∩ s'

Full source

theorem HasBasis.inf_principal (hl : l.HasBasis p s) (s' : Set α) :
    (l ⊓ 𝓟 s').HasBasis p fun i => s i ∩ s' :=
  ⟨fun t => by
    simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]⟩

Basis of Filter Infimum with Principal Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any subset $s' \subseteq \alpha$, the filter $l \sqcap \mathfrak{P}(s')$ has a basis consisting of the sets $s_i \cap s'$ indexed by the same predicate $p$. Here, $\mathfrak{P}(s')$ denotes the principal filter generated by $s'$, and $\sqcap$ denotes the infimum (meet) of two filters.

Filter.HasBasis.principal_inf theorem

(hl : l.HasBasis p s) (s' : Set α) : (𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i

Full source

theorem HasBasis.principal_inf (hl : l.HasBasis p s) (s' : Set α) :
    (𝓟𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i := by
  simpa only [inf_comm, inter_comm] using hl.inf_principal s'

Basis of Principal Filter Infimum with Another Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any subset $s' \subseteq \alpha$, the filter $\mathfrak{P}(s') \sqcap l$ has a basis consisting of the sets $s' \cap s_i$ indexed by the same predicate $p$. Here, $\mathfrak{P}(s')$ denotes the principal filter generated by $s'$, and $\sqcap$ denotes the infimum (meet) of two filters.

Filter.HasBasis.inf_basis_neBot_iff theorem

 (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : NeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃i'⦄, p' i' → (s i ∩ s' i').Nonempty

Full source

theorem HasBasis.inf_basis_neBot_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    NeBotNeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃i'⦄, p' i' → (s i ∩ s' i').Nonempty :=
  (hl.inf' hl').neBot_iff.trans <| by simp [@forall_swap _ ι']

Non-triviality Criterion for Infimum of Two Filters with Bases: $\text{NeBot } (l \sqcap l') \leftrightarrow \forall i i', p(i) \land p'(i') \to s(i) \cap s'(i') \neq \emptyset$

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, $s' : \iota' \to \text{Set } \alpha$. Then the infimum filter $l \sqcap l'$ is non-trivial (i.e., $\text{NeBot } (l \sqcap l')$) if and only if for every pair of indices $(i, i')$ such that $p(i)$ and $p'(i')$ hold, the intersection $s(i) \cap s'(i')$ is nonempty.

Filter.HasBasis.inf_neBot_iff theorem

(hl : l.HasBasis p s) : NeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃s'⦄, s' ∈ l' → (s i ∩ s').Nonempty

Full source

theorem HasBasis.inf_neBot_iff (hl : l.HasBasis p s) :
    NeBotNeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃s'⦄, s' ∈ l' → (s i ∩ s').Nonempty :=
  hl.inf_basis_neBot_iff l'.basis_sets

Non-triviality Criterion for Infimum of Filter with Another Filter: $\text{NeBot } (l \sqcap l') \leftrightarrow \forall i, p(i) \to \forall s' \in l', s_i \cap s' \neq \emptyset$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. The infimum filter $l \sqcap l'$ is non-trivial (i.e., $\text{NeBot } (l \sqcap l')$) if and only if for every index $i$ such that $p(i)$ holds and for every set $s'$ in the filter $l'$, the intersection $s_i \cap s'$ is nonempty.

Filter.HasBasis.inf_principal_neBot_iff theorem

(hl : l.HasBasis p s) {t : Set α} : NeBot (l ⊓ 𝓟 t) ↔ ∀ ⦃i⦄, p i → (s i ∩ t).Nonempty

Full source

theorem HasBasis.inf_principal_neBot_iff (hl : l.HasBasis p s) {t : Set α} :
    NeBotNeBot (l ⊓ 𝓟 t) ↔ ∀ ⦃i⦄, p i → (s i ∩ t).Nonempty :=
  (hl.inf_principal t).neBot_iff

Non-triviality Criterion for Infimum of Filter and Principal Filter: $\text{NeBot } (l \sqcap \mathfrak{P}(t)) \leftrightarrow \forall i, p(i) \to s_i \cap t \neq \emptyset$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any subset $t \subseteq \alpha$, the filter $l \sqcap \mathfrak{P}(t)$ is non-trivial if and only if for every index $i$ such that $p(i)$ holds, the intersection $s_i \cap t$ is nonempty. Here, $\mathfrak{P}(t)$ denotes the principal filter generated by $t$, and $\sqcap$ denotes the infimum (meet) of two filters.

Filter.HasBasis.disjoint_iff theorem

 (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

Full source

theorem HasBasis.disjoint_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    DisjointDisjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i') :=
  not_iff_not.mp <| by simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
    hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

Disjointness Criterion for Filters with Bases: $\text{Disjoint } l \, l' \leftrightarrow \exists i i', p(i) \land p'(i') \land s(i) \cap s'(i') = \emptyset$

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, $s' : \iota' \to \text{Set } \alpha$. Then $l$ and $l'$ are disjoint if and only if there exist indices $i$ and $i'$ such that $p(i)$ and $p'(i')$ hold, and the sets $s(i)$ and $s'(i')$ are disjoint.

Disjoint.exists_mem_filter_basis theorem

 (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')

Full source

theorem _root_.Disjoint.exists_mem_filter_basis (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') :=
  (hl.disjoint_iff hl').1 h

Existence of Disjoint Basis Sets for Disjoint Filters

Informal description

Let $l$ and $l'$ be two filters on a type $\alpha$ with bases $(p, s)$ and $(p', s')$ respectively, where $p : \iota \to \text{Prop}$, $s : \iota \to \text{Set } \alpha$, $p' : \iota' \to \text{Prop}$, $s' : \iota' \to \text{Set } \alpha$. If $l$ and $l'$ are disjoint, then there exist indices $i$ and $i'$ such that $p(i)$ and $p'(i')$ hold, and the sets $s(i)$ and $s'(i')$ are disjoint.

Filter.inf_neBot_iff theorem

: NeBot (l ⊓ l') ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s'⦄, s' ∈ l' → (s ∩ s').Nonempty

Full source

theorem inf_neBot_iff :
    NeBotNeBot (l ⊓ l') ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s'⦄, s' ∈ l' → (s ∩ s').Nonempty :=
  l.basis_sets.inf_neBot_iff

Non-triviality Criterion for Filter Infimum: $\text{NeBot } (l \sqcap l') \leftrightarrow \forall s \in l, \forall s' \in l', s \cap s' \neq \emptyset$

Informal description

The infimum of two filters $l$ and $l'$ on a type $\alpha$ is non-trivial (i.e., $\text{NeBot } (l \sqcap l')$) if and only if for every set $s \in l$ and every set $s' \in l'$, the intersection $s \cap s'$ is nonempty.

Filter.inf_principal_neBot_iff theorem

{s : Set α} : NeBot (l ⊓ 𝓟 s) ↔ ∀ U ∈ l, (U ∩ s).Nonempty

Full source

theorem inf_principal_neBot_iff {s : Set α} : NeBotNeBot (l ⊓ 𝓟 s) ↔ ∀ U ∈ l, (U ∩ s).Nonempty :=
  l.basis_sets.inf_principal_neBot_iff

Non-triviality Criterion for Infimum of Filter and Principal Filter: $\text{NeBot } (l \sqcap \mathfrak{P}(s)) \leftrightarrow \forall U \in l, U \cap s \neq \emptyset$

Informal description

For any filter $l$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the infimum filter $l \sqcap \mathfrak{P}(s)$ is non-trivial if and only if for every set $U \in l$, the intersection $U \cap s$ is nonempty. Here, $\mathfrak{P}(s)$ denotes the principal filter generated by $s$, and $\sqcap$ denotes the infimum (meet) of two filters.

Filter.mem_iff_inf_principal_compl theorem

{f : Filter α} {s : Set α} : s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Full source

theorem mem_iff_inf_principal_compl {f : Filter α} {s : Set α} : s ∈ fs ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥ := by
  refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)
  exact
    ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
      inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩

Membership Criterion via Infimum with Complement Principal Filter: $s \in f \leftrightarrow f \sqcap \mathfrak{P}(s^c) = \bot$

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ belongs to $f$ if and only if the infimum of $f$ and the principal filter generated by the complement $s^c$ is the bottom filter (i.e., the trivial filter containing all sets).

Filter.not_mem_iff_inf_principal_compl theorem

{f : Filter α} {s : Set α} : s ∉ f ↔ NeBot (f ⊓ 𝓟 sᶜ)

Full source

theorem not_mem_iff_inf_principal_compl {f : Filter α} {s : Set α} : s ∉ fs ∉ f ↔ NeBot (f ⊓ 𝓟 sᶜ) :=
  (not_congr mem_iff_inf_principal_compl).trans neBot_iff.symm

Non-membership Criterion via Infimum with Complement Principal Filter: $s \notin f \leftrightarrow f \sqcap \mathfrak{P}(s^c) \neq \bot$

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ does not belong to $f$ if and only if the infimum of $f$ and the principal filter generated by the complement $s^c$ is a nontrivial filter (i.e., not equal to the bottom filter).

Filter.disjoint_principal_right theorem

{f : Filter α} {s : Set α} : Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Full source

@[simp]
theorem disjoint_principal_right {f : Filter α} {s : Set α} : DisjointDisjoint f (𝓟 s) ↔ sᶜ ∈ f := by
  rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

Disjointness Criterion for Filter and Principal Filter: $f \sqcap \mathfrak{P}(s) = \bot \leftrightarrow s^c \in f$

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the filter $f$ is disjoint from the principal filter $\mathfrak{P}(s)$ if and only if the complement $s^c$ belongs to $f$.

Filter.disjoint_principal_left theorem

{f : Filter α} {s : Set α} : Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Full source

@[simp]
theorem disjoint_principal_left {f : Filter α} {s : Set α} : DisjointDisjoint (𝓟 s) f ↔ sᶜ ∈ f := by
  rw [disjoint_comm, disjoint_principal_right]

Disjointness Criterion for Principal Filter and Filter: $\mathfrak{P}(s) \perp f \leftrightarrow s^c \in f$

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the principal filter $\mathfrak{P}(s)$ is disjoint from $f$ if and only if the complement $s^c$ belongs to $f$.

Filter.disjoint_principal_principal theorem

{s t : Set α} : Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Full source

@[simp 1100] -- Porting note: higher priority for linter
theorem disjoint_principal_principal {s t : Set α} : DisjointDisjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t := by
  rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]

Disjointness of Principal Filters: $\mathfrak{P}(s) \perp \mathfrak{P}(t) \leftrightarrow s \cap t = \emptyset$

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, the principal filters $\mathfrak{P}(s)$ and $\mathfrak{P}(t)$ are disjoint if and only if the sets $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).

Filter.disjoint_pure_pure theorem

{x y : α} : Disjoint (pure x : Filter α) (pure y) ↔ x ≠ y

Full source

@[simp]
theorem disjoint_pure_pure {x y : α} : DisjointDisjoint (pure x : Filter α) (pure y) ↔ x ≠ y := by
  simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

Disjointness of Principal Filters: $\text{pure }x \perp \text{pure }y \leftrightarrow x \neq y$

Informal description

For any elements $x$ and $y$ of type $\alpha$, the principal filters generated by $\{x\}$ and $\{y\}$ are disjoint if and only if $x \neq y$.

Filter.HasBasis.disjoint_iff_left theorem

(h : l.HasBasis p s) : Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

Full source

theorem HasBasis.disjoint_iff_left (h : l.HasBasis p s) :
    DisjointDisjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l' := by
  simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
    (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]

Disjointness Criterion for Filters via Basis and Complement: $\text{Disjoint } l \, l' \leftrightarrow \exists i, p(i) \land s(i)^c \in l'$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$ (i.e., $l$ has basis $(p, s)$). Then $l$ is disjoint from another filter $l'$ if and only if there exists an index $i$ such that $p_i$ holds and the complement of $s_i$ belongs to $l'$.

Filter.HasBasis.disjoint_iff_right theorem

(h : l.HasBasis p s) : Disjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

Full source

theorem HasBasis.disjoint_iff_right (h : l.HasBasis p s) :
    DisjointDisjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l' :=
  disjoint_comm.trans h.disjoint_iff_left

Disjointness Criterion for Filters via Basis and Complement (Symmetric Version): $\text{Disjoint } l' \, l \leftrightarrow \exists i, p(i) \land s(i)^c \in l'$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$ (i.e., $l$ has basis $(p, s)$). Then another filter $l'$ is disjoint from $l$ if and only if there exists an index $i$ such that $p_i$ holds and the complement of $s_i$ belongs to $l'$.

Filter.le_iff_forall_inf_principal_compl theorem

{f g : Filter α} : f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥

Full source

theorem le_iff_forall_inf_principal_compl {f g : Filter α} : f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
  forall₂_congr fun _ _ => mem_iff_inf_principal_compl

Filter Refinement Criterion via Infimum with Complement Principal Filters: $f \leq g \leftrightarrow \forall V \in g, f \sqcap \mathfrak{P}(V^c) = \bot$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the filter $f$ is finer than $g$ (i.e., $f \leq g$) if and only if for every set $V$ in $g$, the infimum of $f$ and the principal filter generated by the complement of $V$ is the trivial filter (i.e., $f \sqcap \mathfrak{P}(V^c) = \bot$).

Filter.inf_neBot_iff_frequently_left theorem

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

Full source

theorem inf_neBot_iff_frequently_left {f g : Filter α} :
    NeBotNeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x := by
  simp only [inf_neBot_iff, frequently_iff, and_comm]; rfl

Non-trivial Infimum of Filters via Frequent Predicates

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the infimum $f \sqcap g$ is non-trivial if and only if for every predicate $p : \alpha \to \mathrm{Prop}$, whenever $p$ holds frequently in $f$, then $p$ also holds frequently in $g$.

Filter.inf_neBot_iff_frequently_right theorem

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

Full source

theorem inf_neBot_iff_frequently_right {f g : Filter α} :
    NeBotNeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in g, p x) → ∃ᶠ x in f, p x := by
  rw [inf_comm]
  exact inf_neBot_iff_frequently_left

Non-trivial Infimum of Filters via Frequent Predicates (Symmetric Version)

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the infimum $f \sqcap g$ is non-trivial if and only if for every predicate $p : \alpha \to \mathrm{Prop}$, whenever $p$ holds frequently in $g$, then $p$ also holds frequently in $f$.

Filter.hasBasis_iInf_principal theorem

{s : ι → Set α} (h : Directed (· ≥ ·) s) [Nonempty ι] : (⨅ i, 𝓟 (s i)).HasBasis (fun _ => True) s

Full source

theorem hasBasis_iInf_principal {s : ι → Set α} (h : Directed (· ≥ ·) s) [Nonempty ι] :
    (⨅ i, 𝓟 (s i)).HasBasis (fun _ => True) s :=
  ⟨fun t => by
    simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t⟩

Basis for Infimum of Principal Filters on a Directed Family of Sets

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by a nonempty type $\iota$, and suppose this family is directed with respect to reverse inclusion (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $s_k \subseteq s_i$ and $s_k \subseteq s_j$). Then the infimum filter $\bigsqcap_{i} \mathcal{P}(s_i)$ has a basis consisting of all sets $s_i$ in the family.

Filter.hasBasis_biInf_principal theorem

 {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o (· ≥ ·)) S) (ne : S.Nonempty) :
  (⨅ i ∈ S, 𝓟 (s i)).HasBasis (fun i => i ∈ S) s

Full source

theorem hasBasis_biInf_principal {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o (· ≥ ·)) S)
    (ne : S.Nonempty) : (⨅ i ∈ S, 𝓟 (s i)).HasBasis (fun i => i ∈ S) s :=
  ⟨fun t => by
    refine mem_biInf_of_directed ?_ ne
    rw [directedOn_iff_directed, ← directed_comp] at h ⊢
    refine h.mono_comp _ ?_
    exact fun _ _ => principal_mono.2⟩

Basis for Infimum of Principal Filters on a Directed Family of Sets

Informal description

Let $\{s_i\}_{i \in \beta}$ be a family of subsets of $\alpha$ indexed by a set $\beta$, and let $S \subseteq \beta$ be a nonempty subset. Suppose the family $\{s_i\}_{i \in S}$ is directed with respect to the reverse inclusion relation (i.e., for any $i, j \in S$, there exists $k \in S$ such that $s_k \subseteq s_i$ and $s_k \subseteq s_j$). Then the filter $\bigsqcap_{i \in S} \mathcal{P}(s_i)$ has a basis consisting of the sets $\{s_i\}_{i \in S}$.

Filter.hasBasis_biInf_principal' theorem

 {ι : Type*} {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), 𝓟 (s i)).HasBasis p s

Full source

theorem hasBasis_biInf_principal' {ι : Type*} {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), 𝓟 (s i)).HasBasis p s :=
  Filter.hasBasis_biInf_principal h ne

Basis for Infimum of Principal Filters on a Directed Family Modulo Predicate

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by a type $\iota$, and let $p : \iota \to \mathrm{Prop}$ be a predicate on $\iota$. Suppose that for any indices $i$ and $j$ satisfying $p(i)$ and $p(j)$, there exists an index $k$ satisfying $p(k)$ such that $s_k \subseteq s_i$ and $s_k \subseteq s_j$ (i.e., the family is directed modulo $p$). Additionally, assume there exists at least one index $i$ for which $p(i)$ holds. Then the filter $\bigsqcap_{i \in \iota, p(i)} \mathcal{P}(s_i)$ has a basis consisting of the sets $\{s_i\}_{i \in \iota}$ where $p(i)$ holds.

Filter.HasBasis.map theorem

(f : α → β) (hl : l.HasBasis p s) : (l.map f).HasBasis p fun i => f '' s i

Full source

theorem HasBasis.map (f : α → β) (hl : l.HasBasis p s) : (l.map f).HasBasis p fun i => f '' s i :=
  ⟨fun t => by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩

Basis Characterization of Image Filter: $(l.\text{map}\,f).\text{HasBasis}\,p\,(f(s_i))$

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). For any function $f : \alpha \to \beta$, the image filter $l.map f$ on $\beta$ has a basis consisting of the images $f(s_i)$ for the same index set and predicate. In other words, a set $t \subseteq \beta$ belongs to $l.map f$ if and only if there exists an index $i$ such that $p(i)$ holds and $f(s_i) \subseteq t$.

Filter.HasBasis.comap theorem

(f : β → α) (hl : l.HasBasis p s) : (l.comap f).HasBasis p fun i => f ⁻¹' s i

Full source

theorem HasBasis.comap (f : β → α) (hl : l.HasBasis p s) :
    (l.comap f).HasBasis p fun i => f ⁻¹' s i :=
  ⟨fun t => by
    simp only [mem_comap', hl.mem_iff]
    refine exists_congr (fun i => Iff.rfl.and ?_)
    exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩⟩

Basis Characterization of Filter Preimage: $(l.\text{comap}\,f).\text{HasBasis}\,p\,(f^{-1} \circ s)$

Informal description

Let $l$ be a filter on $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$ (i.e., $l$ has the basis $(p, s)$). For any function $f : \beta \to \alpha$, the filter $l.\text{comap}\,f$ on $\beta$ has a basis consisting of the preimages $f^{-1}(s_i)$ for all indices $i$ such that $p(i)$ holds.

Filter.comap_hasBasis theorem

(f : α → β) (l : Filter β) : HasBasis (comap f l) (fun s : Set β => s ∈ l) fun s => f ⁻¹' s

Full source

theorem comap_hasBasis (f : α → β) (l : Filter β) :
    HasBasis (comap f l) (fun s : Set β => s ∈ l) fun s => f ⁻¹' s :=
  ⟨fun _ => mem_comap⟩

Basis Characterization of Filter Preimage: $(\text{comap}\,f\,l).\text{HasBasis}\,(s \in l)\,f^{-1}(s)$

Informal description

For any function $f : \alpha \to \beta$ and any filter $l$ on $\beta$, the filter `comap f l` on $\alpha$ has a basis consisting of the preimages $f^{-1}(s)$ for all sets $s$ in $l$. In other words, a set $t$ belongs to `comap f l` if and only if there exists a set $s \in l$ such that $f^{-1}(s) \subseteq t$.

Filter.HasBasis.forall_mem_mem theorem

(h : HasBasis l p s) {x : α} : (∀ t ∈ l, x ∈ t) ↔ ∀ i, p i → x ∈ s i

Full source

theorem HasBasis.forall_mem_mem (h : HasBasis l p s) {x : α} :
    (∀ t ∈ l, x ∈ t) ↔ ∀ i, p i → x ∈ s i := by
  simp only [h.mem_iff, exists_imp, and_imp]
  exact ⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩

Characterization of Universal Membership in a Filter Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. For any element $x \in \alpha$, the following are equivalent: 1. $x$ belongs to every set in the filter $l$. 2. For every index $i$, if $p(i)$ holds, then $x \in s_i$.

Filter.HasBasis.biInf_mem theorem

 [CompleteLattice β] {f : Set α → β} (h : HasBasis l p s) (hf : Monotone f) : ⨅ t ∈ l, f t = ⨅ (i) (_ : p i), f (s i)

Full source

protected theorem HasBasis.biInf_mem [CompleteLattice β] {f : Set α → β} (h : HasBasis l p s)
    (hf : Monotone f) : ⨅ t ∈ l, f t = ⨅ (i) (_ : p i), f (s i) :=
  le_antisymm (le_iInf₂ fun i hi => iInf₂_le (s i) (h.mem_of_mem hi)) <|
    le_iInf₂ fun _t ht =>
      let ⟨i, hpi, hi⟩ := h.mem_iff.1 ht
      iInf₂_le_of_le i hpi (hf hi)

Infimum over Filter Basis Equals Infimum over Basis Sets

Informal description

Let $\beta$ be a complete lattice, $l$ a filter on a type $\alpha$ with basis $(p, s)$, and $f : \mathcal{P}(\alpha) \to \beta$ a monotone function. Then the infimum of $f$ over all sets in $l$ equals the infimum of $f$ over the basis sets, i.e., \[ \bigsqcap_{t \in l} f(t) = \bigsqcap_{\substack{i \\ p(i)}} f(s_i). \]

Filter.HasBasis.biInter_mem theorem

{f : Set α → Set β} (h : HasBasis l p s) (hf : Monotone f) : ⋂ t ∈ l, f t = ⋂ (i) (_ : p i), f (s i)

Full source

protected theorem HasBasis.biInter_mem {f : Set α → Set β} (h : HasBasis l p s) (hf : Monotone f) :
    ⋂ t ∈ l, f t = ⋂ (i) (_ : p i), f (s i) :=
  h.biInf_mem hf

Intersection over Filter Basis Equals Intersection over Basis Sets

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$, and let $f : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ be a monotone function. Then the intersection of $f(t)$ over all sets $t$ in $l$ equals the intersection of $f(s_i)$ over all indices $i$ for which $p(i)$ holds, i.e., \[ \bigcap_{t \in l} f(t) = \bigcap_{\substack{i \\ p(i)}} f(s_i). \]

Filter.HasBasis.ker theorem

(h : HasBasis l p s) : l.ker = ⋂ (i) (_ : p i), s i

Full source

protected theorem HasBasis.ker (h : HasBasis l p s) : l.ker = ⋂ (i) (_ : p i), s i :=
  sInter_eq_biInter.trans <| h.biInter_mem monotone_id

Kernel of a Filter Equals Intersection of Basis Sets

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. Then the kernel of $l$, defined as the intersection of all sets in $l$, equals the intersection of all basis sets $s_i$ for which $p(i)$ holds, i.e., \[ \ker l = \bigcap_{\substack{i \\ p(i)}} s_i. \]

Filter.IsAntitoneBasis structure

extends IsBasis (fun _ => True) s''

Full source

/-- `IsAntitoneBasis s` means the image of `s` is a filter basis such that `s` is decreasing. -/
structure IsAntitoneBasis : Prop extends IsBasis (fun _ => True) s'' where
  /-- The sequence of sets is antitone. -/
  protected antitone : Antitone s''

Antitone filter basis

Informal description

A structure `IsAntitoneBasis s` indicates that the image of the function `s` forms a filter basis where `s` is decreasing (antitone). Specifically, it means that the collection of sets `s i` for all indices `i` satisfies the filter basis property (nonempty intersections) and that `s` is order-reversing (i.e., `i ≤ j` implies `s j ⊆ s i`).

Filter.HasAntitoneBasis structure

(l : Filter α) (s : ι'' → Set α) : Prop
    extends HasBasis l (fun _ => True) s

Full source

/-- 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. -/
structure HasAntitoneBasis (l : Filter α) (s : ι'' → Set α) : Prop
    extends HasBasis l (fun _ => True) s where
  /-- The sequence of sets is antitone. -/
  protected antitone : Antitone s

Filter with antitone basis

Informal description

A filter $l$ on a type $\alpha$ is said to have an antitone basis $s : \iota \to \text{Set} \alpha$ if a set $t$ belongs to $l$ if and only if $t$ contains $s(i)$ for some index $i$, and the basis $s$ is decreasing (i.e., $s(i) \supseteq s(j)$ whenever $i \leq j$).

Filter.HasAntitoneBasis.map theorem

 {l : Filter α} {s : ι'' → Set α} (hf : HasAntitoneBasis l s) (m : α → β) : HasAntitoneBasis (map m l) (m '' s ·)

Full source

protected theorem HasAntitoneBasis.map {l : Filter α} {s : ι'' → Set α}
    (hf : HasAntitoneBasis l s) (m : α → β) : HasAntitoneBasis (map m l) (m '' s ·) :=
  ⟨HasBasis.map _ hf.toHasBasis, fun _ _ h => image_subset _ <| hf.2 h⟩

Image Filter of Antitone Basis Preserves Antitone Property

Informal description

Let $l$ be a filter on a type $\alpha$ with an antitone basis $s : \iota \to \text{Set} \alpha$, meaning that $s$ is decreasing (i.e., $s(i) \supseteq s(j)$ whenever $i \leq j$) and a set $t$ belongs to $l$ if and only if $t$ contains $s(i)$ for some index $i$. For any function $m : \alpha \to \beta$, the image filter $\text{map}\,m\,l$ on $\beta$ has an antitone basis given by the images $m(s(i))$ for each index $i$.

Filter.HasAntitoneBasis.comap theorem

 {l : Filter α} {s : ι'' → Set α} (hf : HasAntitoneBasis l s) (m : β → α) : HasAntitoneBasis (comap m l) (m ⁻¹' s ·)

Full source

protected theorem HasAntitoneBasis.comap {l : Filter α} {s : ι'' → Set α}
    (hf : HasAntitoneBasis l s) (m : β → α) : HasAntitoneBasis (comap m l) (m ⁻¹' s ·) :=
  ⟨hf.1.comap _, fun _ _ h ↦ preimage_mono (hf.2 h)⟩

Antitone Basis Preservation under Filter Preimage

Informal description

Let $l$ be a filter on a type $\alpha$ with an antitone basis $s : \iota \to \text{Set} \alpha$, meaning that $s$ is decreasing (i.e., $s(i) \supseteq s(j)$ whenever $i \leq j$) and a set $t$ belongs to $l$ if and only if $t$ contains $s(i)$ for some index $i$. For any function $m : \beta \to \alpha$, the filter $\text{comap}\,m\,l$ on $\beta$ has an antitone basis consisting of the preimages $m^{-1}(s(i))$ for all indices $i \in \iota$.

Filter.HasAntitoneBasis.iInf_principal theorem

 {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)] {s : ι → Set α} (hs : Antitone s) :
  (⨅ i, 𝓟 (s i)).HasAntitoneBasis s

Full source

lemma HasAntitoneBasis.iInf_principal {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    {s : ι → Set α} (hs : Antitone s) : (⨅ i, 𝓟 (s i)).HasAntitoneBasis s :=
  ⟨hasBasis_iInf_principal hs.directed_ge, hs⟩

Antitone Basis for Infimum of Principal Filters

Informal description

Let $\iota$ be a nonempty directed preorder and $\{s_i\}_{i \in \iota}$ be an antitone family of subsets of $\alpha$ (i.e., $i \leq j$ implies $s_j \subseteq s_i$). Then the infimum filter $\bigsqcap_{i} \mathcal{P}(s_i)$ has an antitone basis given by the family $\{s_i\}_{i \in \iota}$.

Filter.HasBasis.tendsto_left_iff theorem

(hla : la.HasBasis pa sa) : Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Full source

theorem HasBasis.tendsto_left_iff (hla : la.HasBasis pa sa) :
    TendstoTendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t := by
  simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]
  rfl

Tendsto Criterion via Basis Elements: $f$ tends to $l_b$ along $l_a$ iff for every $t \in l_b$, $\exists i, p_i \land f(s_i) \subseteq t$

Informal description

Let $l_a$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$, and let $l_b$ be a filter on $\beta$. A function $f : \alpha \to \beta$ tends to $l_b$ along $l_a$ if and only if for every set $t \in l_b$, there exists an index $i$ such that $p_i$ holds and $f$ maps $s_i$ into $t$.

Filter.HasBasis.tendsto_right_iff theorem

(hlb : lb.HasBasis pb sb) : Tendsto f la lb ↔ ∀ i, pb i → ∀ᶠ x in la, f x ∈ sb i

Full source

theorem HasBasis.tendsto_right_iff (hlb : lb.HasBasis pb sb) :
    TendstoTendsto f la lb ↔ ∀ i, pb i → ∀ᶠ x in la, f x ∈ sb i := by
  simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]

Tendsto Criterion via Basis Elements: $f$ tends to $l_b$ along $l_a$ iff for every basis element $s_i$ of $l_b$, $f^{-1}(s_i)$ is eventually in $l_a$

Informal description

Let $l_b$ be a filter on a type $\beta$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$. A function $f : \alpha \to \beta$ tends to $l_b$ along a filter $l_a$ on $\alpha$ if and only if for every index $i$ such that $p_i$ holds, the set of points $x \in \alpha$ for which $f(x) \in s_i$ is eventually in $l_a$.

Filter.HasBasis.tendsto_iff theorem

 (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

Full source

theorem HasBasis.tendsto_iff (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
    TendstoTendsto f la lb ↔ ∀ ib, pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib := by
  simp [hlb.tendsto_right_iff, hla.eventually_iff]

Tendsto Criterion via Basis Elements: $f$ tends to $l_b$ along $l_a$ iff for every basis element $s_j^b$ of $l_b$, there exists a basis element $s_i^a$ of $l_a$ such that $f$ maps $s_i^a$ into $s_j^b$

Informal description

Let $l_a$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i^a$ indexed by a predicate $p_i^a$, and let $l_b$ be a filter on $\beta$ with a basis consisting of sets $s_j^b$ indexed by a predicate $p_j^b$. A function $f : \alpha \to \beta$ tends to $l_b$ along $l_a$ if and only if for every index $j$ such that $p_j^b$ holds, there exists an index $i$ such that $p_i^a$ holds and for all $x \in s_i^a$, $f(x) \in s_j^b$.

Filter.Tendsto.basis_left theorem

(H : Tendsto f la lb) (hla : la.HasBasis pa sa) : ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Full source

theorem Tendsto.basis_left (H : Tendsto f la lb) (hla : la.HasBasis pa sa) :
    ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t :=
  hla.tendsto_left_iff.1 H

Tendsto Implies Basis Mapping: $f$ maps basis sets of $l_a$ into sets of $l_b$

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. Suppose $l_a$ has a basis consisting of sets $s_i$ indexed by a predicate $p_i$. If $f$ tends to $l_b$ along $l_a$, then for every set $t \in l_b$, there exists an index $i$ such that $p_i$ holds and $f$ maps $s_i$ into $t$.

Filter.Tendsto.basis_right theorem

(H : Tendsto f la lb) (hlb : lb.HasBasis pb sb) : ∀ i, pb i → ∀ᶠ x in la, f x ∈ sb i

Full source

theorem Tendsto.basis_right (H : Tendsto f la lb) (hlb : lb.HasBasis pb sb) :
    ∀ i, pb i → ∀ᶠ x in la, f x ∈ sb i :=
  hlb.tendsto_right_iff.1 H

Tendsto Criterion via Basis Elements: $f$ maps eventually into basis sets of $l_b$

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. Suppose $l_b$ has a basis consisting of sets $s_i$ indexed by a predicate $p_i$. If $f$ tends to $l_b$ along $l_a$, then for every index $i$ such that $p_i$ holds, the set of points $x \in \alpha$ for which $f(x) \in s_i$ is eventually in $l_a$.

Filter.Tendsto.basis_both theorem

 (H : Tendsto f la lb) (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
  ∀ ib, pb ib → ∃ ia, pa ia ∧ MapsTo f (sa ia) (sb ib)

Full source

theorem Tendsto.basis_both (H : Tendsto f la lb) (hla : la.HasBasis pa sa)
    (hlb : lb.HasBasis pb sb) :
    ∀ ib, pb ib → ∃ ia, pa ia ∧ MapsTo f (sa ia) (sb ib) :=
  (hla.tendsto_iff hlb).1 H

Tendsto Criterion via Basis Elements: $f$ maps basis sets of $l_a$ into basis sets of $l_b$

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. Suppose $l_a$ has a basis consisting of sets $s_i^a$ indexed by a predicate $p_i^a$, and $l_b$ has a basis consisting of sets $s_j^b$ indexed by a predicate $p_j^b$. If $f$ tends to $l_b$ along $l_a$, then for every index $j$ such that $p_j^b$ holds, there exists an index $i$ such that $p_i^a$ holds and $f$ maps $s_i^a$ into $s_j^b$.

Filter.HasBasis.prod_pprod theorem

 (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
  (la ×ˢ lb).HasBasis (fun i : PProd ι ι' => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2

Full source

theorem HasBasis.prod_pprod (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
    (la ×ˢ lb).HasBasis (fun i : PProd ι ι' => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2 :=
  (hla.comap Prod.fst).inf' (hlb.comap Prod.snd)

Basis Characterization for Product Filter via Pairwise Indexing: $l_a \timesˢ l_b$ has basis $\{s_a(i_1) \times s_b(i_2) \mid p_a(i_1) \land p_b(i_2)\}$

Informal description

Let $l_a$ and $l_b$ be filters on types $\alpha$ and $\beta$ respectively, with bases $(p_a, s_a)$ and $(p_b, s_b)$, where $p_a : \iota \to \text{Prop}$, $s_a : \iota \to \text{Set } \alpha$, $p_b : \iota' \to \text{Prop}$, $s_b : \iota' \to \text{Set } \beta$. Then the product filter $l_a \timesˢ l_b$ has a basis consisting of Cartesian products $s_a(i_1) \times s_b(i_2)$ indexed by pairs $(i_1, i_2) \in \iota \times \iota'$ (represented as `PProd ι ι'`) where both $p_a(i_1)$ and $p_b(i_2)$ hold.

Filter.HasBasis.prod theorem

 {ι ι' : Type*} {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

Full source

theorem HasBasis.prod {ι ι' : Type*} {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 :=
  (hla.comap Prod.fst).inf (hlb.comap Prod.snd)

Basis Characterization for Product Filter via Pairwise Indexing

Informal description

Let $l_a$ and $l_b$ be filters on types $\alpha$ and $\beta$ respectively, with bases $(p_a, s_a)$ and $(p_b, s_b)$, where $p_a : \iota \to \text{Prop}$, $s_a : \iota \to \text{Set } \alpha$, $p_b : \iota' \to \text{Prop}$, $s_b : \iota' \to \text{Set } \beta$. Then the product filter $l_a \timesˢ l_b$ has a basis consisting of Cartesian products $s_a(i_1) \times s_b(i_2)$ indexed by pairs $(i_1, i_2) \in \iota \times \iota'$ where both $p_a(i_1)$ and $p_b(i_2)$ hold.

Filter.HasBasis.principal_prod theorem

(sa : Set α) (h : lb.HasBasis pb sb) : (𝓟 sa ×ˢ lb).HasBasis pb (sa ×ˢ sb ·)

Full source

protected theorem HasBasis.principal_prod (sa : Set α) (h : lb.HasBasis pb sb) :
    (𝓟 sa ×ˢ lb).HasBasis pb (sa ×ˢ sb ·) := by
  simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.snd).principal_inf _

Basis of Principal Filter Product with Another Filter: $\mathfrak{P}(s_a) \timesˢ l_b$ has basis $\{s_a \timesˢ s_b(j) \mid p_b(j)\}$

Informal description

Let $l_b$ be a filter on a type $\beta$ with a basis consisting of sets $s_b(j)$ indexed by a predicate $p_b(j)$. For any subset $s_a \subseteq \alpha$, the product filter $\mathfrak{P}(s_a) \timesˢ l_b$ has a basis consisting of the sets $s_a \timesˢ s_b(j)$ indexed by the same predicate $p_b(j)$. Here, $\mathfrak{P}(s_a)$ denotes the principal filter generated by $s_a$, and $\timesˢ$ denotes the Cartesian product of sets.

Filter.HasBasis.prod_principal theorem

(h : la.HasBasis pa sa) (sb : Set β) : (la ×ˢ 𝓟 sb).HasBasis pa (sa · ×ˢ sb)

Full source

protected theorem HasBasis.prod_principal (h : la.HasBasis pa sa) (sb : Set β) :
    (la ×ˢ 𝓟 sb).HasBasis pa (sa · ×ˢ sb) := by
  simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.fst).inf_principal _

Basis of Product Filter with Principal Filter: $l_a \timesˢ \mathfrak{P}(s_b)$ has basis $\{s_a(i) \timesˢ s_b \mid p_a(i)\}$

Informal description

Let $l_a$ be a filter on a type $\alpha$ with a basis consisting of sets $s_a(i)$ indexed by a predicate $p_a(i)$. For any subset $s_b \subseteq \beta$, the product filter $l_a \timesˢ \mathfrak{P}(s_b)$ has a basis consisting of the sets $s_a(i) \timesˢ s_b$ indexed by the same predicate $p_a(i)$. Here, $\mathfrak{P}(s_b)$ denotes the principal filter generated by $s_b$, and $\timesˢ$ denotes the Cartesian product of sets.

Filter.HasBasis.top_prod theorem

(h : lb.HasBasis pb sb) : (⊤ ×ˢ lb : Filter (α × β)).HasBasis pb (univ ×ˢ sb ·)

Full source

protected theorem HasBasis.top_prod (h : lb.HasBasis pb sb) :
    (⊤ ×ˢ lb : Filter (α × β)).HasBasis pb (univ ×ˢ sb ·) := by
  simpa only [principal_univ] using h.principal_prod univ

Basis of Top Filter Product: $\top \timesˢ l_b$ has basis $\{\alpha \times s_b(j) \mid p_b(j)\}$

Informal description

Let $l_b$ be a filter on a type $\beta$ with a basis consisting of sets $s_b(j)$ indexed by a predicate $p_b(j)$. Then the product filter $\top \timesˢ l_b$ on $\alpha \times \beta$ has a basis consisting of the sets $\alpha \times s_b(j)$ indexed by the same predicate $p_b(j)$, where $\alpha$ denotes the universal set on the type $\alpha$.

Filter.HasBasis.prod_top theorem

(h : la.HasBasis pa sa) : (la ×ˢ ⊤ : Filter (α × β)).HasBasis pa (sa · ×ˢ univ)

Full source

protected theorem HasBasis.prod_top (h : la.HasBasis pa sa) :
    (la ×ˢ ⊤ : Filter (α × β)).HasBasis pa (sa · ×ˢ univ) := by
  simpa only [principal_univ] using h.prod_principal univ

Basis of Product Filter with Top Filter: $l_a \timesˢ \top$ has basis $\{s_a(i) \times \beta \mid p_a(i)\}$

Informal description

Let $l_a$ be a filter on a type $\alpha$ with a basis consisting of sets $s_a(i)$ indexed by a predicate $p_a(i)$. Then the product filter $l_a \timesˢ \top$ on $\alpha \times \beta$ has a basis consisting of the sets $s_a(i) \times \beta$ indexed by the same predicate $p_a(i)$, where $\beta$ denotes the universal set on the type $\beta$.

Filter.HasBasis.prod_same_index theorem

 {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

Full source

theorem HasBasis.prod_same_index {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 := by
  simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]
  refine fun t => ⟨?_, ?_⟩
  · rintro ⟨⟨i, j⟩, ⟨hi, hj⟩, hsub : sa i ×ˢ sb j ⊆ t⟩
    rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
    exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩
  · rintro ⟨i, hi, h⟩
    exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩

Basis for Product Filter with Shared Index and Directed Condition

Informal description

Let $l_a$ and $l_b$ be filters on types $\alpha$ and $\beta$ respectively, both with bases indexed by the same predicate $p : \iota \to \text{Prop}$ and sets $s_a : \iota \to \text{Set } \alpha$ and $s_b : \iota \to \text{Set } \beta$. Suppose that for any indices $i, j$ where $p(i)$ and $p(j)$ hold, there exists an index $k$ such that $p(k)$ holds and $s_a(k) \subseteq s_a(i)$ and $s_b(k) \subseteq s_b(j)$. Then the product filter $l_a \timesˢ l_b$ has a basis consisting of the Cartesian products $s_a(i) \times s_b(i)$ indexed by the same predicate $p$.

Filter.HasBasis.prod_same_index_mono theorem

 {ι : Type*} [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

Full source

theorem HasBasis.prod_same_index_mono {ι : Type*} [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 :=
  hla.prod_same_index hlb fun {i j} hi hj =>
    have : p (min i j) := min_rec' _ hi hj
    ⟨min i j, this, hsa this hi <| min_le_left _ _, hsb this hj <| min_le_right _ _⟩

Basis for Product Filter with Shared Index and Monotone Basis Functions

Informal description

Let $\iota$ be a linearly ordered type, and let $p : \iota \to \text{Prop}$ be a predicate. Suppose $l_a$ and $l_b$ are filters on types $\alpha$ and $\beta$ respectively, both with bases consisting of sets $s_a(i)$ and $s_b(i)$ indexed by $p(i)$. If the functions $s_a$ and $s_b$ are monotone on the subset $\{i \mid p(i)\}$, then the product filter $l_a \timesˢ l_b$ has a basis consisting of the Cartesian products $s_a(i) \times s_b(i)$ indexed by the same predicate $p$.

Filter.HasBasis.prod_same_index_anti theorem

 {ι : Type*} [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

Full source

theorem HasBasis.prod_same_index_anti {ι : Type*} [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 :=
  @HasBasis.prod_same_index_mono _ _ _ _ ιᵒᵈ _ _ _ _ hla hlb hsa.dual_left hsb.dual_left

Basis for Product Filter with Shared Index and Antitone Basis Functions

Informal description

Let $\iota$ be a linearly ordered type, and let $p : \iota \to \text{Prop}$ be a predicate. Suppose $l_a$ and $l_b$ are filters on types $\alpha$ and $\beta$ respectively, both with bases consisting of sets $s_a(i)$ and $s_b(i)$ indexed by $p(i)$. If the functions $s_a$ and $s_b$ are antitone on the subset $\{i \mid p(i)\}$, then the product filter $l_a \timesˢ l_b$ has a basis consisting of the Cartesian products $s_a(i) \times s_b(i)$ indexed by the same predicate $p$.

Filter.HasBasis.prod_self theorem

(hl : la.HasBasis pa sa) : (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i

Full source

theorem HasBasis.prod_self (hl : la.HasBasis pa sa) :
    (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i :=
  hl.prod_same_index hl fun {i j} hi hj => by
    simpa only [exists_prop, subset_inter_iff] using
      hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

Basis for Self-Product Filter via Cartesian Squares of Basis Sets

Informal description

Let $l_a$ be a filter on a type $\alpha$ with a basis consisting of sets $s_a(i)$ indexed by a predicate $p_a(i)$. Then the product filter $l_a \timesˢ l_a$ has a basis consisting of the Cartesian products $s_a(i) \times s_a(i)$ indexed by the same predicate $p_a(i)$.

Filter.mem_prod_self_iff theorem

{s} : s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s

Full source

theorem mem_prod_self_iff {s} : s ∈ la ×ˢ las ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s :=
  la.basis_sets.prod_self.mem_iff

Membership Criterion for Self-Product Filter via Cartesian Squares

Informal description

For any set $s$ in the product filter $l_a \timesˢ l_a$ on $\alpha \times \alpha$, there exists a set $t \in l_a$ such that the Cartesian product $t \times t$ is a subset of $s$. Conversely, if such a set $t$ exists, then $s$ belongs to the product filter $l_a \timesˢ l_a$. In other words, a set $s$ is in the product filter $l_a \timesˢ l_a$ if and only if there exists a set $t$ in $l_a$ such that $t \times t \subseteq s$.

Filter.eventually_prod_self_iff theorem

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

Full source

lemma eventually_prod_self_iff {r : α → α → Prop} :
    (∀ᶠ x in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y :=
  mem_prod_self_iff.trans <| by simp only [prod_subset_iff, mem_setOf_eq]

Uniformity Criterion for Binary Relations in Product Filter

Informal description

For any binary relation $r$ on a type $\alpha$ and a filter $l_a$ on $\alpha$, the following are equivalent: 1. The relation $r(x, y)$ holds for all pairs $(x, y)$ in the product filter $l_a \timesˢ l_a$. 2. There exists a set $t \in l_a$ such that for all $x, y \in t$, the relation $r(x, y)$ holds. In other words, $r$ holds eventually in $l_a \timesˢ l_a$ if and only if there exists a set in $l_a$ where $r$ holds uniformly on its Cartesian square.

Filter.eventually_prod_self_iff' theorem

{r : α × α → Prop} : (∀ᶠ x in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y)

Full source

/-- A version of `eventually_prod_self_iff` that is more suitable for forward rewriting. -/
lemma eventually_prod_self_iff' {r : α × α → Prop} :
    (∀ᶠ x in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y) :=
  Iff.symm eventually_prod_self_iff.symm

Uniformity Criterion for Binary Relations in Self-Product Filter

Informal description

For any binary relation $r$ on pairs of elements of type $\alpha$ and a filter $l_a$ on $\alpha$, the following are equivalent: 1. The relation $r(x, y)$ holds for all pairs $(x, y)$ in the product filter $l_a \times l_a$. 2. There exists a set $t \in l_a$ such that for all $x, y \in t$, the relation $r(x, y)$ holds. In other words, $r$ holds eventually in $l_a \times l_a$ if and only if there exists a set in $l_a$ where $r$ holds uniformly on its Cartesian square.

Filter.HasAntitoneBasis.prod theorem

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

Full source

theorem HasAntitoneBasis.prod {ι : Type*} [LinearOrder ι] {f : Filter α} {g : Filter β}
    {s : ι → Set α} {t : ι → Set β} (hf : HasAntitoneBasis f s) (hg : HasAntitoneBasis g t) :
    HasAntitoneBasis (f ×ˢ g) fun n => s n ×ˢ t n :=
  ⟨hf.1.prod_same_index_anti hg.1 (hf.2.antitoneOn _) (hg.2.antitoneOn _), hf.2.set_prod hg.2⟩

Antitone Basis for Product Filter via Cartesian Products

Informal description

Let $\iota$ be a linearly ordered type, and let $f$ and $g$ be filters on types $\alpha$ and $\beta$ respectively. Suppose $f$ has an antitone basis $s : \iota \to \text{Set } \alpha$ (i.e., $s$ is decreasing and $t \in f$ if and only if $t$ contains $s(i)$ for some $i$), and $g$ has an antitone basis $t : \iota \to \text{Set } \beta$. Then the product filter $f \timesˢ g$ has an antitone basis given by the Cartesian products $s(n) \times t(n)$ for $n \in \iota$.

Filter.HasBasis.coprod theorem

 {ι ι' : Type*} {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

Full source

theorem HasBasis.coprod {ι ι' : Type*} {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.fstProd.fst ⁻¹' sa i.1Prod.fst ⁻¹' sa i.1 ∪ Prod.snd ⁻¹' sb i.2 :=
  (hla.comap Prod.fst).sup (hlb.comap Prod.snd)

Coproduct Filter Basis Characterization: $l_a \sqcup l_b$ has basis $\{f^{-1}(s_a(i)) \cup g^{-1}(s_b(j))\}_{p_a(i) \land p_b(j)}$

Informal description

Let $l_a$ and $l_b$ be filters on types $\alpha$ and $\beta$ respectively, with bases $(p_a, s_a)$ and $(p_b, s_b)$, where $p_a : \iota \to \text{Prop}$, $s_a : \iota \to \text{Set } \alpha$, $p_b : \iota' \to \text{Prop}$, and $s_b : \iota' \to \text{Set } \beta$. Then the coproduct filter $l_a \sqcup l_b$ has a basis indexed by pairs $(i,j) \in \iota \times \iota'$ where $p_a(i)$ and $p_b(j)$ both hold, and the corresponding basis sets are the unions of the preimages $f^{-1}(s_a(i)) \cup g^{-1}(s_b(j))$, where $f$ and $g$ are the canonical projections from $\alpha \times \beta$ to $\alpha$ and $\beta$ respectively. In other words, a set belongs to $l_a \sqcup l_b$ if and only if it contains a union of preimages $f^{-1}(s_a(i)) \cup g^{-1}(s_b(j))$ for some indices $i$ and $j$ satisfying $p_a(i)$ and $p_b(j)$ respectively.

Filter.map_sigma_mk_comap theorem

 {π : α → Type*} {π' : β → Type*} {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)

Full source

theorem map_sigma_mk_comap {π : α → Type*} {π' : β → Type*} {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) := by
  refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_
  convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
  apply image_sigmaMk_preimage_sigmaMap hf

Equality of Filter Constructions via Sigma Mapping for Injective Index Function

Informal description

Let $f \colon \alpha \to \beta$ be an injective function, and for each $a \in \alpha$, let $g_a \colon \pi_a \to \pi'_{f(a)}$ be a function. For any $a \in \alpha$ and any filter $l$ on $\pi'_{f(a)}$, the filter obtained by first taking the preimage of $l$ under $g_a$ and then mapping with the embedding $\Sigma.mk_a$ is equal to the filter obtained by first mapping $l$ with the embedding $\Sigma.mk_{f(a)}$ and then taking the preimage under the map $\Sigma.map \, f \, g$. In symbols: \[ \text{map}\,(\Sigma.mk_a)\,(\text{comap}\,(g_a)\,l) = \text{comap}\,(\Sigma.map\,f\,g)\,(\text{map}\,(\Sigma.mk_{f(a)})\,l). \]

Mathlib.Order.Filter.Bases.Basic

Main statements

Implementation notes

Main statements