lowerSemicontinuousWithinAt_const
theorem lowerSemicontinuousWithinAt_const :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {x : α} {s : Set α} {z : β},
LowerSemicontinuousWithinAt (fun _x => z) s x
The theorem `lowerSemicontinuousWithinAt_const` states that for any topological space `α`, any preordered set `β`, any element `x` of `α`, any set `s` of `α` and any element `z` of `β`, a function that is constant at `z` is lower semicontinuous at `x` within the set `s`. In mathematical terms, given any `y < z`, for all points `x'` sufficiently close to `x` in `s`, we have `y < z`. This is because the value of the function at any point is always `z`, regardless of where the point is located within the topological space.
More concisely: For any topological space α, preordered set β, point x in α, set s in α, and constant function f(y) = z from β to ℝ, if x ∈ s then f is lower semicontinuous at x if and only if for all y < z, there exists ε > 0 such that for all x' in s with d(x, x') < ε, we have y ≤ f(x').
|
LowerSemicontinuous.add'
theorem LowerSemicontinuous.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
LowerSemicontinuous f →
LowerSemicontinuous g →
(∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → LowerSemicontinuous fun z => f z + g z
The theorem `LowerSemicontinuous.add'` states that if we have two functions, `f` and `g`, that are lower semicontinuous within a topological space, and the addition operation is continuous at each point of these functions, then the sum of these two functions is also lower semicontinuous. Here, lower semicontinuous means that for any `x`, and for any `y < f x` or `g x`, there exists a neighborhood of `x` such that for all points `x'` in this neighborhood, `f x'` or `g x'` is at least `y`. The continuity of addition ensures that the sum of `f` and `g` is well-behaved, that is, if we take a point `x` and its neighborhood, the sum of `f` and `g` at these points tends to the sum of `f x` and `g x` as the points tend to `x`.
More concisely: If two lower semicontinuous functions `f` and `g` with continuous addition have the property that for all `x`, the set `{y : y < f x ∨ y < g x}` has a neighborhood where `f` and `g` are both greater than or equal to `y`, then their sum `f + g` is also lower semicontinuous.
|
UpperSemicontinuousOn.add'
theorem UpperSemicontinuousOn.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
UpperSemicontinuousOn f s →
UpperSemicontinuousOn g s →
(∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → UpperSemicontinuousOn (fun z => f z + g z) s
The theorem `UpperSemicontinuousOn.add'` states that if `f` and `g` are two functions that are upper semicontinuous on a set `s` of some type `α` equipped with a topological space structure, and that output values in a linearly ordered additive commutative monoid `γ` with an order topology, then their pointwise sum is also upper semicontinuous on `s`, provided that the operation of addition is continuous at each point in `s`. In other words, for each point `x` in `s`, if the values of `f` and `g` at `x` and nearby points never exceed `f(x)` and `g(x)` by more than some small positive amount, respectively, then the same is true for the sum of `f` and `g`.
More concisely: If `f` and `g` are upper semicontinuous functions on a set `s` with values in an additive commutative monoid `γ` equipped with an order topology, and the addition operation is continuous on `s`, then their pointwise sum is upper semicontinuous on `s`.
|
UpperSemicontinuousWithinAt.add
theorem UpperSemicontinuousWithinAt.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4}
[inst_1 : LinearOrderedAddCommMonoid γ] [inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ]
[inst_4 : ContinuousAdd γ] {f g : α → γ},
UpperSemicontinuousWithinAt f s x →
UpperSemicontinuousWithinAt g s x → UpperSemicontinuousWithinAt (fun z => f z + g z) s x
The theorem states that the sum of two upper semicontinuous functions is upper semicontinuous. More specifically, given two functions `f` and `g` that are upper semicontinuous at a point `x` within a set `s`, the function that maps any point `z` to the sum `f z + g z` is also upper semicontinuous at `x` within `s`. This is formulated in a general topological space with a linearly ordered additive commutative monoid structure, and assumes that the addition operation is continuous. The theorem is also applicable to extended real numbers, with the use of the primed version of the lemma with an explicit continuity assumption on addition.
More concisely: If `f` and `g` are upper semicontinuous functions at a point `x` in a topological space with a linearly ordered additive commutative monoid structure and continuous addition, then their sum `f + g` is upper semicontinuous at `x`.
|
lowerSemicontinuousAt_ciSup
theorem lowerSemicontinuousAt_ciSup :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5}
[inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
(∀ᶠ (y : α) in nhds x, BddAbove (Set.range fun i => f i y)) →
(∀ (i : ι), LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
The theorem `lowerSemicontinuousAt_ciSup` states that for a topological space `α`, a point `x` from that space, and a conditionally complete linear order `δ'`, if a function `f` mapping from some index set `ι` to `α` to `δ'` satisfies two conditions: (1) for all points `y` in a neighborhood of `x`, the range of function values is bounded above, and (2) the function `f` is lower semicontinuous at `x` for each index `i`, then the supremum function which takes `x'` to the supremum of `f i x'` over all `i`, is also lower semicontinuous at `x`.
In other words, if each function in a family of functions is lower semicontinuous at a point and the family is bounded above in a neighborhood of that point, then the function that gives the supremum of the family at each point is also lower semicontinuous at the given point.
More concisely: If a family of lower semicontinuous functions from a topological space to a conditionally complete linear order, each bounded above in a neighborhood of a point, has a supremum function that is also defined and bounded at that point, then the supremum function is lower semicontinuous at the point.
|
IsOpen.upperSemicontinuous_indicator
theorem IsOpen.upperSemicontinuous_indicator :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {s : Set α} {y : β}
[inst_2 : Zero β], IsOpen s → y ≤ 0 → UpperSemicontinuous (s.indicator fun _x => y)
This theorem states that for any topological space `α`, preordered set `β`, specific set `s` of type `α`, and a value `y` of type `β` with `β` as zero, if the set `s` is open and `y` is less than or equal to zero, then the indicator function (which gives `y` when the input is in set `s` and `0` otherwise) is upper semicontinuous. An upper semicontinuous function is one where for any `ε > 0`, for any `x`, for all `x'` close enough to `x`, `f x'` is at most `f x + ε`. In simpler terms, this means that the indicator function does not jump upwards - it's either constant or decreasing - when we restrict to an open set and a non-positive constant value.
More concisely: For any topological space `α`, preordered set `β` with `β` as zero, open set `s` in `α`, and value `y` in `β`, if `s` is open and `y` is less than or equal to zero, then the indicator function of `s` is upper semicontinuous at `y`.
|
UpperSemicontinuous.add
theorem UpperSemicontinuous.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
UpperSemicontinuous f → UpperSemicontinuous g → UpperSemicontinuous fun z => f z + g z
The theorem `UpperSemicontinuous.add` states that if we have two functions `f` and `g` that are upper semicontinuous (meaning that for any value `x` and any `y > f(x)`, there exists a neighborhood around `x` such that for all points `x'` in this neighborhood, `f(x') ≤ y`), then the function that maps any input `z` to `f(z) + g(z)` is also upper semicontinuous. This theorem is specifically formulated in the context of a topological space with a linear ordered additive commutative monoid structure, where addition is continuous. This theorem is also applicable to extended real numbers (`EReal`).
More concisely: If `f` and `g` are upper semicontinuous functions on a topological space with a linear ordered additive commutative monoid structure where addition is continuous, then their sum `f + g` is also upper semicontinuous.
|
lowerSemicontinuousWithinAt_ciSup
theorem lowerSemicontinuousWithinAt_ciSup :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ' : Type u_5}
[inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
(∀ᶠ (y : α) in nhdsWithin x s, BddAbove (Set.range fun i => f i y)) →
(∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
This theorem, `lowerSemicontinuousWithinAt_ciSup`, states that in a given topological space with a conditionally complete linear order, for a set `s` of type `α` and an element `x` of the same type, if for each element `y` in a neighborhood within `s` of `x`, the range of the function `f i y` is bounded above, and for each index `i`, the function `f i` is lower semicontinuous at `x` within `s`, then the function defined by taking the supremum over `i` of `f i x'` for all `x'` is also lower semicontinuous at `x` within `s`. In other words, the lower semicontinuity is preserved under taking the supremum of a family of functions if each function in that family is lower semicontinuous and the set of values of these functions is bounded above in the neighborhood of the point of interest within the set.
More concisely: If each function in a family of lower semicontinuous functions with bounded above ranges is applied to elements in a neighborhood of a point in a conditional complete linear order, then the supremum of these functions is also lower semicontinuous at that point.
|
LowerSemicontinuous.add
theorem LowerSemicontinuous.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
LowerSemicontinuous f → LowerSemicontinuous g → LowerSemicontinuous fun z => f z + g z
The theorem states that if we have two lower semicontinuous functions, say `f` and `g`, then the function that is the sum of these two, for any input `z`, is also lower semicontinuous. This is formulated within a topological space with a linear ordered additive commutative monoid structure, and assumes that addition operation is continuous. In mathematical terms, a function `f` is lower semicontinuous at a point `x` if for all `y < f(x)`, there exists a neighborhood of `x` such that for all points `x'` in this neighborhood, `f(x') ≥ y`.
More concisely: If `f` and `g` are lower semicontinuous functions on a topological space with a linear ordered additive commutative monoid structure where addition is continuous, then their sum is also lower semicontinuous.
|
UpperSemicontinuousOn.add
theorem UpperSemicontinuousOn.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
UpperSemicontinuousOn f s → UpperSemicontinuousOn g s → UpperSemicontinuousOn (fun z => f z + g z) s
This theorem states that the sum of two upper semicontinuous functions is also upper semicontinuous. Specifically, if we have a topological space `α`, a set `s` of `α`, a linear ordered additive commutative monoid `γ` with a topological structure and an order topology, and a continuous addition operation on `γ`, then if `f` and `g` are two upper semicontinuous functions from `α` to `γ` defined on the set `s`, the function `(fun z => f z + g z)` that maps each element `z` in `s` to the sum of `f(z)` and `g(z)` is also upper semicontinuous on `s`.
More concisely: If `f` and `g` are upper semicontinuous functions from a topological space `α` to an ordered additive commutative monoid `γ` with a topology and continuous addition, then their sum `(z => f z + g z)` is also upper semicontinuous on `α`.
|
UpperSemicontinuousWithinAt.add'
theorem UpperSemicontinuousWithinAt.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4}
[inst_1 : LinearOrderedAddCommMonoid γ] [inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
UpperSemicontinuousWithinAt f s x →
UpperSemicontinuousWithinAt g s x →
ContinuousAt (fun p => p.1 + p.2) (f x, g x) → UpperSemicontinuousWithinAt (fun z => f z + g z) s x
The theorem states that, given two functions `f` and `g` in a topological space `α` that are upper semicontinuous at a point `x` within a set `s`, and given that the addition of the function values `(f x, g x)` is continuous at the point `x`, then the function obtained by adding `f` and `g` pointwise, i.e., the function `z -> f z + g z`, is also upper semicontinuous at the point `x` within the set `s`. Here, `γ` is a linearly ordered additive commutative monoid equipped with a topological space structure and an order topology. The upper semicontinuity is a property indicating that for any value `y` greater than the function value at `x`, there exists a neighborhood around `x` within the set `s` where all function values are less than `y`. The requirement of continuity of addition is explicitly stated, making the theorem applicable to extended real numbers (`EReal`).
More concisely: Given two upper semicontinuous functions `f` and `g` on a topological space `α` at a point `x` within a set `s`, with the addition of their values being continuous at `x`, the pointwise sum `z => f z + g z` is also upper semicontinuous at `x` within `s` in an additive commutative monoid `γ` with order topology.
|
UpperSemicontinuousAt.add
theorem UpperSemicontinuousAt.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
UpperSemicontinuousAt f x → UpperSemicontinuousAt g x → UpperSemicontinuousAt (fun z => f z + g z) x
The theorem `UpperSemicontinuousAt.add` states that for any topological space `α`, any point `x` in `α`, and any linear ordered additive commutative monoid `γ` that also forms a topological space with an order topology, if addition in `γ` is continuous, then the sum of two functions `f` and `g` from `α` to `γ` that are upper semicontinuous at `x` is also upper semicontinuous at `x`. In other words, if for any `y` greater than `f(x)` or `g(x)`, all points `x'` close enough to `x` satisfy `f(x') < y` and `g(x') < y` respectively, then for any `y` greater than `(f+g)(x)`, all points close enough to `x` satisfy `(f+g)(x') < y`.
This theorem is also formulated with the `ContinuousAdd` assumption, and is useful for numerical applications such as `EReal`.
More concisely: Given a topological space `α`, a point `x` in `α`, and two upper semicontinuous functions `f` and `g` from `α` to a linear ordered additive commutative monoid `γ` with an order topology and continuous addition, the sum `f + g` is also upper semicontinuous at `x`.
|
UpperSemicontinuous.upperSemicontinuousWithinAt
theorem UpperSemicontinuous.upperSemicontinuousWithinAt :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {f : α → β},
UpperSemicontinuous f → ∀ (s : Set α) (x : α), UpperSemicontinuousWithinAt f s x
This theorem states that for all types `α`, which have a topology, and `β`, which have a preorder, and for any function `f` from `α` to `β`, if `f` is UpperSemicontinuous, then for any set `s` of type `α` and any element `x` of `α`, `f` is also UpperSemicontinuousWithinAt `s` at `x`. In mathematical terms, the upper semicontinuity of a real-valued function in the entire space guarantees its upper semicontinuity at any point within any subset of that space.
More concisely: For any type `α` with a topology and `β` with a preorder, if the function `f` from `α` to `β` is upper semicontinuous, then it is upper semicontinuous within `s` at every `x` in `α`.
|
Mathlib.Topology.Semicontinuous._auxLemma.7
theorem Mathlib.Topology.Semicontinuous._auxLemma.7 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) = ∀ (x : α), ¬p x
This theorem, `Mathlib.Topology.Semicontinuous._auxLemma.7`, states that for any type `α` and any predicate `p` on `α`, the statement "there doesn't exist an element `x` in `α` such that `p(x)` holds" is equivalent to "for all elements `x` in `α`, `p(x)` doesn't hold". In mathematical notation, this can be written as ¬(∃x in α, p(x)) is equivalent to ∀x in α, ¬p(x).
More concisely: The negation of the existence of an element in a type satisfying a predicate is equivalent to the universally quantified negation of the predicate for all elements in the type.
|
IsClosed.upperSemicontinuous_indicator
theorem IsClosed.upperSemicontinuous_indicator :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {s : Set α} {y : β}
[inst_2 : Zero β], IsClosed s → 0 ≤ y → UpperSemicontinuous (s.indicator fun _x => y)
The theorem `IsClosed.upperSemicontinuous_indicator` states that for any type `α` equipped with a topology, any preordered type `β` with a zero element, any closed set `s` of type `α`, and any non-negative `y` of type `β`, the function defined by the set indicator of `s` with constant value `y` is upper semicontinuous. In other words, for every `ε > 0` and every `x`, if any element `x'` is close enough to `x`, then the value of the indicator function at `x'` is at most the value of the indicator function at `x` plus `ε`. This indicator function returns `y` if the input element is in the set `s`, and `0` otherwise.
More concisely: For any closed set `s` in a topological space `α` and any non-negative `y`, the set indicator function of `s` with constant value `y` is upper semicontinuous.
|
LowerSemicontinuousOn.add'
theorem LowerSemicontinuousOn.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
LowerSemicontinuousOn f s →
LowerSemicontinuousOn g s →
(∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → LowerSemicontinuousOn (fun z => f z + g z) s
The theorem `LowerSemicontinuousOn.add'` states that in a topological space `α` and a set `s` within `α`, if you have two functions `f` and `g` that map from `α` to a `γ` (where `γ` is a linear ordered additive commutative monoid with a topological space structure and order topology), and both `f` and `g` are lower semicontinuous on `s`, then the sum function (which adds the outputs of `f` and `g`) is also lower semicontinuous on `s`. This is under the assumption that the addition of `f(x)` and `g(x)` is a continuous function at each point `x` in the set `s`.
More concisely: If `f` and `g` are lower semicontinuous functions from a topological space `α` to a linear ordered additive commutative monoid `γ` with a topological space structure and order topology, and their sum is a continuous function on `s Պ α`, then the sum function is lower semicontinuous on `s`.
|
UpperSemicontinuousAt.add'
theorem UpperSemicontinuousAt.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
UpperSemicontinuousAt f x →
UpperSemicontinuousAt g x →
ContinuousAt (fun p => p.1 + p.2) (f x, g x) → UpperSemicontinuousAt (fun z => f z + g z) x
This theorem states that if we have two functions `f` and `g` which are upper semicontinuous at a point `x` in a topological space, and the operation of addition is continuous at the pair `(f x, g x)`, then the sum function, which maps each point `z` to `f z + g z`, is also upper semicontinuous at `x`. In other words, for any value `γ` greater than `(f z + g z)`, there exists a neighborhood around `x` such that for all points in this neighborhood, the sum of the function values at these points is less than `γ`. The theorem is formulated with an explicit assumption on the continuity of addition, which is useful for application to extended real numbers (`EReal`).
More concisely: If `f` and `g` are upper semicontinuous functions at `x` in a topological space and addition is continuous at `(f x, g x)`, then the sum `z => f z + g z` is also upper semicontinuous at `x`.
|
LowerSemicontinuousAt.add'
theorem LowerSemicontinuousAt.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
LowerSemicontinuousAt f x →
LowerSemicontinuousAt g x →
ContinuousAt (fun p => p.1 + p.2) (f x, g x) → LowerSemicontinuousAt (fun z => f z + g z) x
The theorem `LowerSemicontinuousAt.add'` states that the sum of two lower semicontinuous functions is also lower semicontinuous at a given point under certain conditions. Specifically, for any topological space `α`, point `x` in `α`, and linearly ordered, additive, and commutative monoid `γ` equipped with a topology and an ordering that makes it an ordered topological space, if `f` and `g` are functions from `α` to `γ` that are lower semicontinuous at `x` and the function that adds pairs of elements from `γ` is continuous at the point `(f x, g x)`, then the function that maps `z` in `α` to the sum `f z + g z` is lower semicontinuous at `x`. This is given with an explicit continuity assumption on addition, intended for application to `EReal`. The version of the theorem without the prime uses a `ContinuousAdd` instance instead.
More concisely: If `f` and `g` are lower semicontinuous functions at a point `x` in a topological space `α`, and the addition function is continuous at `(f x, g x)` in the ordered topological space `(γ, +, ≤)`, then the function `z ↦ f z + g z` is lower semicontinuous at `x`.
|
LowerSemicontinuousWithinAt.add
theorem LowerSemicontinuousWithinAt.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4}
[inst_1 : LinearOrderedAddCommMonoid γ] [inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ]
[inst_4 : ContinuousAdd γ] {f g : α → γ},
LowerSemicontinuousWithinAt f s x →
LowerSemicontinuousWithinAt g s x → LowerSemicontinuousWithinAt (fun z => f z + g z) s x
The theorem 'LowerSemicontinuousWithinAt.add' asserts that for a given set 's' and a point 'x' within a topological space 'α', and for an ordered additive commutative monoid 'γ' that has a topological structure and an order topology, if the addition operation is continuous and if two functions 'f' and 'g' from 'α' to 'γ' are both lower semicontinuous at 'x' within 's', then the function that adds the outputs of 'f' and 'g' is also lower semicontinuous at 'x' within 's'. In other words, the lower semicontinuity property is preserved under the addition of two lower semicontinuous functions.
More concisely: If two lower semicontinuous functions from a topological space to an ordered additive commutative monoid with a topology, whose addition operation is continuous, are given, then their sum is also lower semicontinuous.
|
Mathlib.Topology.Semicontinuous._auxLemma.10
theorem Mathlib.Topology.Semicontinuous._auxLemma.10 : (¬False) = True
This theorem states that the negation of 'False' is 'True'. In the context of logic, a statement is either true or false. Therefore, if a statement is not false, it necessarily must be true. This is a fundamental concept in logic and boolean algebra.
More concisely: The negation of False is True. (or equivalently, False implies True)
|
IsClosed.lowerSemicontinuous_indicator
theorem IsClosed.lowerSemicontinuous_indicator :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {s : Set α} {y : β}
[inst_2 : Zero β], IsClosed s → y ≤ 0 → LowerSemicontinuous (s.indicator fun _x => y)
This theorem states that for any type `α` which has a topology, type `β` that is equipped with a preorder and a zero element, a set `s` of type `α`, and a value `y` of type `β`, if the set `s` is closed in the topological space `α`, and `y` is less than or equal to zero, then the indicator function `Set.indicator s (fun _x => y)`, which is defined to be `y` if an element is in the set `s` and zero otherwise, is lower semicontinuous. In the context of analysis, this means that for all `x` in `α`, for any value `z` less than the function's value at `x`, there exists a neighborhood of `x` such that the function's value at any point in this neighborhood is not less than `z`.
More concisely: For any topological space `α` with type `α` having a topology, any preordered type `β` with a zero element, any closed set `s` in `α`, and any `y` in `β` less than or equal to zero, the indicator function `Set.indicator s (fun _x => y)` is lower semicontinuous.
|
ContinuousAt.comp_lowerSemicontinuousWithinAt
theorem ContinuousAt.comp_lowerSemicontinuousWithinAt :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [inst_1 : LinearOrder γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {δ : Type u_4} [inst_4 : LinearOrder δ]
[inst_5 : TopologicalSpace δ] [inst_6 : OrderTopology δ] {g : γ → δ} {f : α → γ},
ContinuousAt g (f x) → LowerSemicontinuousWithinAt f s x → Monotone g → LowerSemicontinuousWithinAt (g ∘ f) s x
The theorem `ContinuousAt.comp_lowerSemicontinuousWithinAt` states that, given a set `s` of elements of some type `α` in a topological space, a point `x` in `α`, and functions `f : α → γ` and `g : γ → δ`, where `γ` and `δ` are both linear orders equipped with a topological structure and an order topology. If `g` is continuous at the point `f(x)`, `f` is lower semicontinuous at the point `x` within the set `s`, and `g` is monotone, then the composition of `g` and `f` (i.e., `g ∘ f`), is also lower semicontinuous at the point `x` within the set `s`.
In simple terms, the continuity of a function `g` at `f(x)`, the lower semicontinuity of another function `f` at `x` within a set `s`, and the monotonicity of `g`, together preserve the property of lower semicontinuity for the composition of `g` and `f` at `x` within `s`.
More concisely: If a function `f : α → γ` is lower semicontinuous at a point `x ∈ α` in a set `s ⊆ α`, `g : γ → δ` is continuous at `f(x)` and monotone, then their composition `g ∘ f` is lower semicontinuous at `x` within `s`.
|
lowerSemicontinuousWithinAt_iSup
theorem lowerSemicontinuousWithinAt_iSup :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4}
[inst_1 : CompleteLinearOrder δ] {f : ι → α → δ},
(∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
The theorem `lowerSemicontinuousWithinAt_iSup` states that for any topological space `α`, any point `x` in that space, any set `s` of elements of `α`, any type `ι`, any complete linear order `δ`, and any function `f` from `ι` and `α` to `δ`, if every `f i` is lower semicontinuous at `x` within `s`, then the function that maps `x'` to the supremum (least upper bound) over all `i` of `f i x'` is also lower semicontinuous at `x` within `s`. In simpler terms, the supremum of a collection of lower semicontinuous functions is also lower semicontinuous.
More concisely: If each function in a collection of lower semicontinuous functions from a topological space to a complete linear order is lower semicontinuous at a point, then their supremum function is also lower semicontinuous at that point.
|
LowerSemicontinuous.lowerSemicontinuousWithinAt
theorem LowerSemicontinuous.lowerSemicontinuousWithinAt :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {f : α → β},
LowerSemicontinuous f → ∀ (s : Set α) (x : α), LowerSemicontinuousWithinAt f s x
The theorem `LowerSemicontinuous.lowerSemicontinuousWithinAt` states that for any type `α` with a topological space structure, any type `β` with a preorder structure, and any function `f` from `α` to `β`, if the function `f` is lower semicontinuous, then for any set `s` of type `α` and any element `x` of type `α`, `f` is lower semicontinuous at `x` within the set `s`. In more mathematical terms, if for any `ε > 0`, for all `x'` sufficiently close to `x`, `f(x')` is at least `f(x) - ε`, then this property still holds when we restrict our attention to `x'` values within a certain set `s`.
More concisely: If `f` is a lower semicontinuous function from a topological space `α` to a preordered type `β`, then for any set `s` and any point `x` in `α`, `f` is lower semicontinuous at `x` within `s`, i.e., for every `ε > 0`, there exists a neighborhood `N` of `x` in `s` such that for all `x'` in `N`, `f(x') ≥ f(x) - ε`.
|
LowerSemicontinuousOn.add
theorem LowerSemicontinuousOn.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
LowerSemicontinuousOn f s → LowerSemicontinuousOn g s → LowerSemicontinuousOn (fun z => f z + g z) s
The theorem `LowerSemicontinuousOn.add` states that the sum of two lower semicontinuous functions on a set is also lower semicontinuous. More formally, given any topological space `α`, a set `s` of `α`, a linearly ordered additive commutative monoid `γ` with a defined topological structure and order topology, and a continuous addition operation on `γ`, if `f` and `g` are two functions from `α` to `γ` that are both lower semicontinuous on `s`, then the function defined as the sum of `f` and `g`, for each element in `s`, is also lower semicontinuous on `s`. The rule is formulated with the assumption of continuous addition and is also applicable to extended real numbers (`EReal`).
More concisely: If `f` and `g` are two lower semicontinuous functions from a set `s` in a topological space to an additive commutative monoid with continuous addition, then their sum is also lower semicontinuous on `s`.
|
LowerSemicontinuousWithinAt.add'
theorem LowerSemicontinuousWithinAt.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4}
[inst_1 : LinearOrderedAddCommMonoid γ] [inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
LowerSemicontinuousWithinAt f s x →
LowerSemicontinuousWithinAt g s x →
ContinuousAt (fun p => p.1 + p.2) (f x, g x) → LowerSemicontinuousWithinAt (fun z => f z + g z) s x
The theorem states: Given two functions `f` and `g` from a topological space `α` to a linearly ordered, additive commutative monoid `γ` (also a topological space), if both `f` and `g` are lower semicontinuous at a point `x` within a set `s`, and the addition operation is continuous at the pair `(f x, g x)`, then the function `z ↦ f z + g z` is also lower semicontinuous at `x` within the set `s`. In simpler terms, the sum of two lower semicontinuous functions is also lower semicontinuous, under these conditions.
More concisely: If `f` and `g` are lower semicontinuous functions from a topological space `α` to a linearly ordered, additive commutative monoid `γ` (also a topological space), and their addition is continuous, then the function `z ↦ f z + g z` is lower semicontinuous.
|
LowerSemicontinuousAt.add
theorem LowerSemicontinuousAt.add :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] [inst_4 : ContinuousAdd γ] {f g : α → γ},
LowerSemicontinuousAt f x → LowerSemicontinuousAt g x → LowerSemicontinuousAt (fun z => f z + g z) x
The theorem states that if two functions, `f` and `g`, are lower semicontinuous at a point `x`, then their sum is also lower semicontinuous at `x`. This is formulated in a general topological space with a continuous addition operation. Lower semicontinuity at a point means that, for any number `y` less than the function value at `x`, all points `x'` sufficiently close to `x` have function values greater than `y`. The theorem asserts that this property is preserved under addition of two such functions.
More concisely: If two lower semicontinuous functions `f` and `g` are defined on a topological space and are defined and finite at a point `x`, then their sum `f + g` is also lower semicontinuous at `x`.
|
lowerSemicontinuousWithinAt_sum
theorem lowerSemicontinuousWithinAt_sum :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {γ : Type u_4}
[inst_1 : LinearOrderedAddCommMonoid γ] [inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ]
[inst_4 : ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι},
(∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) →
LowerSemicontinuousWithinAt (fun z => a.sum fun i => f i z) s x
This theorem states that if we have a topological space `α`, a point `x` in `α`, a set `s` of `α`, a finite set `a` of indices of type `ι`, and a family of functions `f` from `ι` and `α` to a linear ordered additive commutative monoid `γ` that also has a topological structure, order topology and continuous addition, then if every function `f i` is lower semicontinuous at point `x` within set `s` for every index `i` in the finite set `a`, the sum function, which at each point `z` of `α` sums over all `f i z` for each `i` in `a`, is also lower semicontinuous at `x` within `s`.
In simple terms, the lower semicontinuity within a set is preserved when taking the sum of a finite number of lower semicontinuous functions.
More concisely: If `α` is a topological space, `x` is a point in `α`, `s` is a set in `α`, `a` is a finite index set, and `f` is a family of lower semicontinuous functions from `α x ι` to a topological monoid `γ`, then the sum function from `α` to `γ` defined as the pointwise sum of `f i` is lower semicontinuous at `x` within `s`.
|
IsOpen.lowerSemicontinuous_indicator
theorem IsOpen.lowerSemicontinuous_indicator :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : Preorder β] {s : Set α} {y : β}
[inst_2 : Zero β], IsOpen s → 0 ≤ y → LowerSemicontinuous (s.indicator fun _x => y)
The theorem `IsOpen.lowerSemicontinuous_indicator` states that for any type `α` with a topological space structure, any type `β` with a preorder structure and a zero element, any open set `s` of type `α`, and any nonnegative `y` of type `β`, the indicator function of the set `s` that takes value `y` for elements in `s` and `0` for elements not in `s` is lower semicontinuous. In other words, for any `ε > 0`, for any `x` in the topological space, for all `x'` close enough to `x`, then the value of this indicator function at `x'` is at least the value at `x - ε`.
More concisely: Given a topological space (α, t), a preorder (β, ≤) with zero element, an open set s ∈ t(α), and a nonnegative real number y ∈ β, the indicator function of s with value y on s and 0 otherwise is lower semicontinuous.
|
UpperSemicontinuous.add'
theorem UpperSemicontinuous.add' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrderedAddCommMonoid γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {f g : α → γ},
UpperSemicontinuous f →
UpperSemicontinuous g →
(∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → UpperSemicontinuous fun z => f z + g z
The theorem states that the sum of two upper semi-continuous functions is also upper semi-continuous. Here, a function `f` from a topological space `α` to a preordered space `β` is said to be upper semi-continuous if for every point `x` in `α`, for any value `y` greater than `f(x)`, there exists a neighborhood of `x` such that for all points `x'` in this neighborhood, `f(x')` is less than or equal to `y`. This is formulated with an explicit assumption of continuity on addition, applicable to `EReal`. The theorem thus asserts that if `f` and `g` are two upper semi-continuous functions from a topological space `α` to a linearly ordered additive commutative monoid `γ` equipped with a topological structure and an order topology, and if for every `x` the sum of `f(x)` and `g(x)` is continuous, then the function `z => f(z) + g(z)` is upper semi-continuous.
More concisely: If two upper semi-continuous functions from a topological space to a linearly ordered additive commutative monoid with a topological order, whose sum is continuous, are given, then their sum is an upper semi-continuous function.
|
ContinuousAt.comp_lowerSemicontinuousAt
theorem ContinuousAt.comp_lowerSemicontinuousAt :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_3} [inst_1 : LinearOrder γ]
[inst_2 : TopologicalSpace γ] [inst_3 : OrderTopology γ] {δ : Type u_4} [inst_4 : LinearOrder δ]
[inst_5 : TopologicalSpace δ] [inst_6 : OrderTopology δ] {g : γ → δ} {f : α → γ},
ContinuousAt g (f x) → LowerSemicontinuousAt f x → Monotone g → LowerSemicontinuousAt (g ∘ f) x
This theorem states that if we have a function `g` from some ordered topological space `\gamma` to another ordered topological space `\delta`, and another function `f` from a topological space `\alpha` to `\gamma`, then if `g` is continuous at `f(x)` for some `x` in `\alpha`, `f` is lower semicontinuous at `x`, and `g` is monotone, then the composition `g ∘ f` is lower semicontinuous at `x`.
In less formal terms, it says that the composition of a continuous function and a lower semicontinuous function is also lower semicontinuous, assuming that the continuous function is monotone. This is under the condition that the first function is continuous at the point where the second function is lower semicontinuous.
More concisely: If a monotone, continuous function `g` from an ordered topological space `\delta` to another ordered topological space `\gamma`, and a lower semicontinuous function `f` from a topological space `\alpha` to `\gamma` are such that `g` is continuous at `f(x)` for some `x` in `\alpha`, then their composition `g ∘ f` is lower semicontinuous at `x`.
|