continuousWithinAt_Ioi_iff_Ici
theorem continuousWithinAt_Ioi_iff_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [inst_2 : TopologicalSpace β]
{a : α} {f : α → β}, ContinuousWithinAt f (Set.Ioi a) a ↔ ContinuousWithinAt f (Set.Ici a) a
The theorem `continuousWithinAt_Ioi_iff_Ici` states that for any two topological spaces `α` and `β`, where `α` is also a partial order, a function `f` from `α` to `β` is continuous at a point `a` within the right-infinite interval that is open on the left `(Set.Ioi a)` if and only if `f` is continuous at the same point `a` within the right-infinite interval that is closed on the left `(Set.Ici a)`. In other words, the continuity of `f` at `a` over the right-open or right-closed right-infinite intervals is equivalent.
More concisely: For any topological spaces α and β, where α is a partial order, the function f from α to β is continuous at a point a in the right-open interval Ioi a and the right-closed interval Ici a if and only if they are equal in the sense of sets. (That is, continuity of f at a over the two types of right-infinite intervals is interchangeable.)
|
nhds_left_sup_nhds_right
theorem nhds_left_sup_nhds_right :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
nhdsWithin a (Set.Iic a) ⊔ nhdsWithin a (Set.Ici a) = nhds a
This theorem states that for any type `α` considered as a topological space and equipped with a linear order, and for any element `a` of `α`, the supremum (join in the filter lattice) of the "neighborhood within" filters at `a` over the sets of all elements less than or equal to `a` and all elements greater than or equal to `a` equals the neighborhood filter at `a`. In other words, the union of the filters that contain the neighborhoods of `a` within both the left-closed right-infinite interval and the left-infinite right-closed interval gives us the filter that contains the neighborhoods of `a` in the entire space.
More concisely: For any type `α` with a linear order and any element `a` in `α`, the supremum of the neighborhood filters at `a` within the left-closed right-infinite and left-infinite right-closed intervals equals the neighborhood filter at `a`.
|
continuousAt_iff_continuous_left_right
theorem continuousAt_iff_continuous_left_right :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
{a : α} {f : α → β}, ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iic a) a ∧ ContinuousWithinAt f (Set.Ici a) a
The theorem `continuousAt_iff_continuous_left_right` states that, for all types `α` and `β` such that `α` has a topology and a linear order, and `β` has a topology, and for all `a` in `α` and function `f` from `α` to `β`, the function `f` is continuous at point `a` if and only if `f` is continuous at `a` within the left-infinite right-closed interval at `a` (i.e., all `x` such that `x ≤ a`) and `f` is continuous at `a` within the left-closed right-infinite interval at `a` (i.e., all `x` such that `a ≤ x`).
More concisely: A function between ordered topological spaces is continuous at a point if and only if it is continuous on the left-closed, right-infinite intervals at that point.
|