Filter.nhds_eq
theorem Filter.nhds_eq : ∀ {α : Type u_2} (l : Filter α), nhds l = l.lift' (Set.Iic ∘ Filter.principal)
This theorem states that for any type α and any filter `l` on α, the neighborhood filter of `l` is equivalent to the filter obtained by applying the lift' operation to `l` with the function that maps each set to the set of all those elements which are less than or equal to all elements of the principal filter of the set. In other words, the filter of all neighborhoods (sets containing an open subset) at a given point `l` in a topological space is equal to the filter generated by mapping `l` through a process that first generates the principal filter (the collection of all supersets) of a set and then collects all elements that are less than or equal to any element in that principal filter.
More concisely: The neighborhood filter of a filter on a type is equivalent to the filter generated by applying the lift' operation and taking the set of elements less than or equal to each principal filter.
|
Mathlib.Topology.Filter._auxLemma.2
theorem Mathlib.Topology.Filter._auxLemma.2 :
∀ {α : Type u_1} [inst : Preorder α] {b x : α}, (x ∈ Set.Iic b) = (x ≤ b)
This theorem states that for any type `α` that is a preorder, and for any two elements `b` and `x` of this type, `x` belongs to the set `Set.Iic b` if and only if `x` is less than or equal to `b`. In other words, the set `Set.Iic b` is defined to be the set of all elements that are less than or equal to `b`.
More concisely: For any preorder type `α` and elements `b` and `x` of `α`, `x` belongs to `Set.Iic b` if and only if `x ≤ b`.
|
Mathlib.Topology.Filter._auxLemma.3
theorem Mathlib.Topology.Filter._auxLemma.3 :
∀ {α : Type u} {s : Set α} {f : Filter α}, (f ≤ Filter.principal s) = (s ∈ f)
This theorem states that for any type `α`, any set `s` of type `α`, and any filter `f` on `α`, the filter `f` is less than or equal to the principal filter of `s` if and only if the set `s` is a member of the filter `f`. In other words, it is saying that a filter `f` contains all supersets of `s` (which is what it means for `f` to be less than or equal to the principal filter of `s`) if and only if `s` is one of the sets in the filter `f`.
More concisely: For any filter `f` on a type `α` and any set `s` of type `α`, `f` is less than or equal to the principal filter of `s` if and only if `s` is an element of `f`.
|
Filter.HasBasis.nhds
theorem Filter.HasBasis.nhds :
∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → (nhds l).HasBasis p fun i => Set.Iic (Filter.principal (s i))
The theorem `Filter.HasBasis.nhds` states that for any type `ι`, `α`, any filter `l` on `α`, and any two functions `p : ι → Prop` and `s : ι → Set α`, if the filter `l` has a basis characterized by the predicate `p` and the set-valued function `s`, then the neighborhood filter `nhds l` also has a basis characterized by `p` and the function `i ↦ Set.Iic (Filter.principal (s i))`. Here `Set.Iic (Filter.principal (s i))` represents the set of all elements less than or equal to the principal filter generated by `s i`.
More concisely: If a filter on a type has a basis given by a predicate and a set-valued function, then its neighborhood filter also has a basis given by the same predicate and the function mapping each element to the closed interval filter generated by its basis element.
|