nhds_cons
theorem nhds_cons :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (l : List α),
nhds (a :: l) = Seq.seq (List.cons <$> nhds a) fun x => nhds l
This theorem, `nhds_cons`, states that for any type `α` equipped with a topology (denoted by `inst : TopologicalSpace α`) and any element `a` of type `α` and list `l` of type `List α`, the neighborhood filter of the cons list `(a :: l)` is equal to the sequence of the map of list cons function on the neighborhood filter of `a` and the neighborhood filter of `l`. In other words, it shows how the neighborhood filter of a cons list can be constructed from the neighborhood filters of its head and tail.
More concisely: Given a topological space `α` and an element `a` in `α` with neighborhood filter `Nhds a`, and a list `l` of elements in `α` with neighborhood filter `Nhds l`, the neighborhood filter of the cons list `a :: l` is equal to `Nhds a ⊓ ∥map (λx ═> Nhds x) (Nhds l)∥`, where `⊓` denotes the meet operation in the lattice of filters on `α` and `∥map ...∥` denotes the sequential composition of the map function with `map` and the set of filters.
|
nhds_nil
theorem nhds_nil : ∀ {α : Type u_1} [inst : TopologicalSpace α], nhds [] = pure []
The theorem `nhds_nil` states that for any type `α` equipped with a topology, the neighborhood filter of an empty list is equal to a filter that only contains the empty list itself. In other words, in any topological space, the only neighborhood of the empty list is the empty list itself.
More concisely: In any topological space, the neighborhood filter of the empty list is equal to the filter containing only the empty list.
|
Filter.Tendsto.cons
theorem Filter.Tendsto.cons :
∀ {β : Type u_2} [inst : TopologicalSpace β] {α : Type u_3} {f : α → β} {g : α → List β} {a : Filter α} {b : β}
{l : List β},
Filter.Tendsto f a (nhds b) →
Filter.Tendsto g a (nhds l) → Filter.Tendsto (fun a => f a :: g a) a (nhds (b :: l))
This theorem, denoted as `Filter.Tendsto.cons`, states that for any two functions `f` and `g` mapping from a type `α` to a topological space `β` and a list of `β` respectively, and given a filter `a` on `α` and elements `b` of `β` and `l` being a list of `β`, if `f` tends to `b` with respect to filter `a` and `g` tends to `l` with respect to filter `a`, then the function that takes an element of `α` and maps it to the list obtained by adding `f(a)` in front of `g(a)` also tends to the list obtained by adding `b` in front of `l` with respect to filter `a`. In simpler terms, it states that if each function tends to its respective limit under a particular filter, then the function that forms a list by combining the outputs also tends to the list formed by combining the limits.
More concisely: If functions `f : α -> β` and `g : α -> β^List` tend to `b : β` and `l : β^List` respectively under filter `a : Filter α`, then the function that concatenates `[f a]` and `g a` tends to `[b] ++ l` under filter `a`. (Here, `++` denotes list concatenation, `β^List` denotes the type of lists of `β`, and `[x]` denotes the singleton list containing `x`.)
|