Filter.mem_lift_sets
theorem Filter.mem_lift_sets :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β},
Monotone g → ∀ {s : Set β}, s ∈ f.lift g ↔ ∃ t ∈ f, s ∈ g t
This theorem, `Filter.mem_lift_sets`, states that for any types `α` and `β`, any filter `f` of type `Filter α`, and any function `g` from a set of `α` to a filter of `β` that is monotone, a set `s` of type `β` is a member of the filter produced by lifting `f` using `g` if and only if there exists a set `t`, a member of `f`, such that `s` is a member of the filter produced by applying `g` to `t`. In essence, it provides an equivalence condition for membership in a filter obtained by a lifting operation, in terms of the existence of a set in the original filter that maps to the set in question in the lifted filter via the used function.
More concisely: For any filters `f` on type `α` and `g : α → Filter β` monotone functions, a set `s` is in the lifted filter `g''(f)` if and only if there exists `t` in `f` such that `s` is in `g(t)`.
|
Filter.lift_mono
theorem Filter.lift_mono :
∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Set α → Filter β},
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.lift g₁ ≤ f₂.lift g₂
The theorem `Filter.lift_mono` states that for any two types `α` and `β`, two filters `f₁` and `f₂` on `α`, and two functions `g₁` and `g₂` from sets of `α` to filters on `β`, if `f₁` is a subset of `f₂` (i.e., `f₁ ≤ f₂`) and `g₁` is a subset of `g₂` (i.e., `g₁ ≤ g₂`), then the filter obtained by lifting `f₁` via `g₁` is a subset of the filter obtained by lifting `f₂` via `g₂`. In other words, the operation of lifting preserves the subset relationship.
More concisely: Given filters `f₁ ≤ f₂` on type `α` and functions `g₁ : Set α → Filter β` and `g₂ : Set α → Filter β` with `g₁ ≤ g₂`, the lifted filters `Filter.map g₁ f₁` and `Filter.map g₂ f₂` satisfy `Filter.map g₁ f₁ ≤ Filter.map g₂ f₂`.
|
Filter.HasBasis.lift
theorem Filter.HasBasis.lift :
∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
f.HasBasis p s →
∀ {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {g : Set α → Filter γ},
(∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) →
Monotone g → (f.lift g).HasBasis (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
The theorem `Filter.HasBasis.lift` states that if `(p : ι → Prop, s : ι → Set α)` forms a basis of a filter `f`, `g` is a monotone function from `Set α` to `Filter γ`, and for each `i`, `(pg : β i → Prop, sg : β i → Set α)` forms a basis of the filter `g (s i)`, then `(fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (i : ι) (x : β i) ↦ sg i x)` forms a basis of the filter `f.lift g`. This basis is parametrized by `i : ι` and `x : β i`, so to express this fact using `has_basis` one has to use `Σ i, β i` as the index type. Also, there is a `mem_iff` statement corresponding to this, formulated without using a sigma type, which is `Filter.HasBasis.mem_lift_iff`.
More concisely: Given a filter `f` on `α` with basis `(p : ι → Prop, s : ι → Set α)`, a monotone function `g : Set α → Filter γ`, and for each `i`, a basis `(pg : β i → Prop, sg : β i → Set α)` of the filter `g (s i)`, then the pair `(λ (i, x) : Σ i, β i. p i ∧ pg i x, λ (i, x) : Σ i, β i. sg i x)` forms a basis of the lifted filter `f.lift g`.
|
Filter.mem_lift'
theorem Filter.mem_lift' :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {t : Set α}, t ∈ f → h t ∈ f.lift' h
The theorem `Filter.mem_lift'` states that for any types `α` and `β`, any filter `f` on `α`, any function `h` from sets of `α` to sets of `β`, and any set `t` of `α`, if `t` is in the filter `f`, then the image of `t` under `h` is in the lift of the filter `f` along `h`. In layman's terms, this theorem asserts that lifting a filter along a function preserves membership: if a set belongs to the original filter, its image under the function belongs to the lifted filter.
More concisely: If `f` is a filter on `α`, `h` is a function from sets of `α` to sets of `β`, and `t ∈ f`, then `h(t) ∈ lift f at h`.
|
Filter.mem_prod_same_iff
theorem Filter.mem_prod_same_iff :
∀ {α : Type u_1} {la : Filter α} {s : Set (α × α)}, s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
This theorem, referred to as an alias of `Filter.mem_prod_self_iff`, states that for any given type `α`, any filter `la` of `α`, and any set `s` of tuples of `α`, the set `s` is in the product of `la` with itself (`la ×ˢ la`) if and only if there exists a set `t` in `la` such that the product of `t` with itself (`t ×ˢ t`) is a subset of `s`.
More concisely: For any filter `la` on type `α` and any set `s` of tuples of `α`, `s` is in the product `la ×ˢ la` if and only if there exists `t` in `la` such that `t ×ˢ t` is a subset of `s`.
|
Filter.lift'_principal
theorem Filter.lift'_principal :
∀ {α : Type u_1} {β : Type u_2} {h : Set α → Set β} {s : Set α},
Monotone h → (Filter.principal s).lift' h = Filter.principal (h s)
The theorem `Filter.lift'_principal` states that for all types `α` and `β`, a function `h` from sets of `α` to sets of `β`, and a set `s` of type `α`, if `h` is monotone (i.e., preserves the order), then lifting the principal filter of `s` via `h` is equivalent to the principal filter of the set `h(s)`. In simpler terms, applying `h` to each element of the principal filter of `s` (a collection of all supersets of `s`) and then creating a new filter from the results gives the same filter as if we simply applied `h` to `s` and took the principal filter of the result.
More concisely: For all types `α` and `β`, if `h : ℙ(α) → ℙ(β)` is monotone and `s : α`, then `filter.lift h (filter.principal s) = filter.principal (h s)`.
|
Filter.comap_lift_eq2
theorem Filter.comap_lift_eq2 :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Filter γ},
Monotone g → (Filter.comap m f).lift g = f.lift (g ∘ Set.preimage m)
This theorem states that for all types `α`, `β`, and `γ`, given a filter `f` of type `α`, a function `m` mapping `β` to `α`, and a function `g` which maps a set of type `β` to a filter of type `γ`, and assuming that `g` is a monotone function, the filter obtained by lifting the filter `f` comapped through `m` over `g` is equal to the filter obtained by lifting `f` over the composition of `g` and the preimage of `m`. In other words, the operation of "comapping" a filter through a function and then "lifting" it over a monotone function can be rearranged as "lifting" the original filter over the composition of the monotone function and the preimage of the original function. This establishes a certain commutativity property between the "lift" and "comap" operations in the context of filters.
More concisely: Given filters `f` of type `α`, function `m` from `β` to `α`, monotone function `g` from sets of type `β` to filters of type `γ`, the lifting of `f` through `m` over `g` equals the lifting of `f` over `g` composed with the preimage of `m`.
|
Filter.le_lift
theorem Filter.le_lift :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} {h : Filter β},
h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s
The theorem `Filter.le_lift` states that for any types `α` and `β`, any filter `f` on `α`, any function `g` from sets of `α` to filters on `β`, and any filter `h` on `β`, the filter `h` is less than or equal to the filter obtained by lifting `f` via `g` if and only if, for all sets `s` in the filter `f`, `h` is less than or equal to the filter `g(s)`. In other words, it provides a condition for a filter on `β` to be below the push-forward of a filter on `α` along a function mapping each set to a filter.
More concisely: For filters $f$ on type $\alpha$, functions $g$ from sets of $\alpha$ to filters on type $\beta$, and filters $h$ on $\beta$, $h \leq \bigl(\mathop{\mathrm{lift}}_{\alpha \rightarrow \beta} f\bigr) (g) \iff \forall s \in f, h \leq g(s)$.
|
Filter.lift'_bot
theorem Filter.lift'_bot :
∀ {α : Type u_1} {β : Type u_2} {h : Set α → Set β}, Monotone h → ⊥.lift' h = Filter.principal (h ∅)
The theorem `Filter.lift'_bot` states that for all types `α` and `β`, and for any function `h` mapping sets of `α` to sets of `β`, if `h` is a monotone function, then lifting the bottom filter via `h` (essentially applying `h` to each set in the bottom filter) is equivalent to the principal filter of `h` applied to the empty set. In other words, if you consider the smallest possible filter (the empty set), and you map it using a monotone function, you end up with the filter that contains all sets that are supersets of the image of the empty set under `h`. This theorem connects the concepts of monotone functions, the bottom filter, and principal filters in the context of order theory and filter theory.
More concisely: For any monotone function `h` between sets, lifting the bottom filter of `α` through `h` equals the principal filter of `h` on the empty set of `α`.
|
Filter.lift_assoc
theorem Filter.lift_assoc :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {h : Set β → Filter γ},
Monotone g → (f.lift g).lift h = f.lift fun s => (g s).lift h
The theorem `Filter.lift_assoc` states that for any types `α`, `β`, and `γ`, any filter `f` of type `α`, and any two functions `g` and `h` that map from a set of `α` and `β` to filters of `β` and `γ` respectively, if `g` is a monotone function, then the operation of lifting the filter `f` twice, first by `g` and then by `h`, is equivalent to lifting `f` once by a function which first applies `g` to `s` and then lifts the result by `h`. This can be thought of as a form of associativity for the filter lift operation when the intermediate function is monotone.
More concisely: For any monotone functions `g : Filter α -> Filter β` and `h : Filter β -> Filter γ`, if `f : Filter α`, then `(h ∘ g) ( Filter.map g f ) = Filter.map (g ∘ h) f`.
|
Filter.comap_lift'_eq
theorem Filter.comap_lift'_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : γ → β},
Filter.comap m (f.lift' h) = f.lift' (Set.preimage m ∘ h)
This theorem states that for any types `α`, `β`, and `γ`, any filter `f` on `α`, any function `h` from a set of `α` to a set of `β`, and any function `m` from `γ` to `β`, the filter obtained by first applying the lift' operation to `f` with `h` and then taking the `comap` with `m` is the same as the filter obtained by first applying `Set.preimage` with `m` to `h` and then applying the lift' operation to `f`. In other words, `Filter.comap m (Filter.lift' f h)` is equal to `Filter.lift' f (Set.preimage m ∘ h)`. This equivalence establishes a key relationship between the operations of lifting a filter and pre-imaging a set under a function.
More concisely: For any filters `f` on type `α`, functions `h: α → β` and `m: γ → β`, the filters `Filter.comap m (Filter.lift' f h)` and `Filter.lift' f (Set.preimage m ∘ h)` are equal.
|
Filter.HasBasis.mem_lift_iff
theorem Filter.HasBasis.mem_lift_iff :
∀ {α : Type u_1} {γ : Type u_3} {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
f.HasBasis p s →
∀ {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {g : Set α → Filter γ},
(∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) →
Monotone g → ∀ {s : Set γ}, s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
The theorem `Filter.HasBasis.mem_lift_iff` states that given a filter `f` with a basis `(p : ι → Prop, s : ι → Set α)`, a monotone function `g` from `Set α` to `Filter γ`, and for each `i`, a basis `(pg : β i → Prop, sg : β i → Set α)` of the filter `g (s i)`, then the tuple `(fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (i : ι) (x : β i) ↦ sg i x)` is a basis of the filter `f.lift g`. This basis is parameterized by `i : ι` and `x : β i`. In particular, a set `s` belongs to the filter `f.lift g` if and only if there exists an `i` such that `p i` holds and there exists an `x` such that `pg i x` holds and `sg i x` is a subset of `s`. This theorem provides a characterization of membership in the filter `f.lift g` without requiring the use of a sigma type.
More concisely: Given a filter `f` with basis `(p : ι → Prop, s : ι → Set α)`, a monotone function `g : Set α -> Filter γ`, and basis `(pg : β i → Prop, sg : β i → Set α)` for each `i` of the filters `g (s i)`, the tuple `(p i ∧ pg i x, sg i x)` is a basis for `f.lift g`, and a set `s` belongs to `f.lift g` if and only if there exists an `i` and an `x` such that `p i` holds, `pg i x` holds, and `sg i x` is a subset of `s`.
|
Filter.HasBasis.lift'
theorem Filter.HasBasis.lift' :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α},
f.HasBasis p s → Monotone h → (f.lift' h).HasBasis p (h ∘ s)
The theorem `Filter.HasBasis.lift'` states that for any types `α` and `β`, any filter `f` on `α`, any function `h` that maps sets of `α` to sets of `β`, any index type `ι`, any basis predicate `p` on `ι`, and any basis function `s` from `ι` to the sets of `α`, if `f` has a basis determined by the predicate `p` and the function `s`, and if the function `h` is monotone, then the filter obtained by lifting `f` along `h` using the function `Filter.lift'` also has a basis determined by the same predicate `p` and the function `h` composed with `s`. In other words, if we have a basis for a filter and a monotone function, we can "lift" the filter along this function and still have a basis, where the basis function is the composition of the original basis function and the monotone function.
More concisely: If a filter on type `α` has a basis determined by predicate `p` and function `s`, and `h` is a monotone function from sets of `α` to sets of `β`, then the filter obtained by lifting along `h` using `Filter.lift'` also has a basis determined by `p` and the composition of `h` and `s`.
|
Filter.mem_lift'_sets
theorem Filter.mem_lift'_sets :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β},
Monotone h → ∀ {s : Set β}, s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s
This theorem states that for every filter `f` on a type `α` and a monotone function `h` from sets of `α` to sets of `β`, a set `s` of `β` is a member of the filter obtained by lifting `f` along `h` if and only if there exists a set `t` in `f` such that `h` applied to `t` is a subset of `s`. In other words, the theorem provides a necessary and sufficient condition for a set to be in the filter obtained by the `lift'` operation on a filter using a monotone function.
More concisely: A set belongs to the filter obtained by lifting a filter through a monotone function if and only if there exists a set in the filter that maps to a subset of the set.
|
Filter.lift'_mono
theorem Filter.lift'_mono :
∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {h₁ h₂ : Set α → Set β},
f₁ ≤ f₂ → h₁ ≤ h₂ → f₁.lift' h₁ ≤ f₂.lift' h₂
The theorem `Filter.lift'_mono` states that for any two types `α` and `β`, given any two filters `f₁` and `f₂` on `α`, and any two function `h₁` and `h₂` that map a set of `α` to a set of `β`, if filter `f₁` is less than or equal to filter `f₂` (in the sense of a partial order), and function `h₁` is less than or equal to function `h₂` (in the sense of a partial order), then the lift of filter `f₁` via `h₁` is less than or equal to the lift of filter `f₂` via `h₂`. Essentially, this theorem is saying that the `lift'` operation in filter theory preserves the order of both filters and functions.
More concisely: Given filters `f₁` and `f₂` on type `α` and functions `h₁` and `h₂` from `α` to `β`, if `f₁ ≤ f₂` and `h₁ ≤ h₂`, then `h₁⁁ⁱ⁻¹⁁(f₁) ≤ h₂⁁ⁱ⁻¹⁁(f₂)`.
|
Filter.lift_le
theorem Filter.lift_le :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} {h : Filter β} {s : Set α},
s ∈ f → g s ≤ h → f.lift g ≤ h
This theorem is about filters and sets in Lean 4. Specifically, it states that for any types 'α' and 'β', any filter 'f' of type 'α', any function 'g' that maps a set 'α' to a filter 'β', any filter 'h' of type 'β', and any set 's' of type 'α', if 's' is in the filter 'f' and the filter 'g(s)' is less than or equal to the filter 'h', then the lift of filter 'f' along the function 'g' is also less than or equal to the filter 'h'. In other words, the theorem guarantees a certain order-preserving property of the 'lift' operation on filters.
More concisely: For any filters $f:\alpha \to Prop$, $g:\alpha \to \beta \to Prop$, and $h:\beta \to Prop$, if $s:\alpha$, $f(s)$, and $g(s,\_) \leq h$ hold, then $lift(f,g) \leq h$, where $lift(f,g) : \beta \to Prop$ is the lift of filter $f$ along function $g$.
|
Filter.le_lift'
theorem Filter.le_lift' :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {g : Filter β},
g ≤ f.lift' h ↔ ∀ s ∈ f, h s ∈ g
This theorem states that for any given types `α` and `β`, a filter `f` on `α`, a function `h` from the set of `α` to the set of `β`, and a filter `g` on `β`, the filter `g` is less than or equal to the lift of filter `f` through function `h` if and only if for all sets `s` in the filter `f`, the image of the set `s` under the function `h` is in the filter `g`. In other words, this theorem establishes the condition under which a filter on `β` is considered to be below (or equal to) the push-forward of a filter on `α` via a function mapping sets of `α` to sets of `β`.
More concisely: A filter `g` on `β` is less than or equal to the lift of filter `f` on `α` through function `h` if and only if for all sets `s` in `f`, `h(`s`) ∈ g`.
|