IsExposed.eq_inter_halfspace'
theorem IsExposed.eq_inter_halfspace' :
β {π : Type u_1} {E : Type u_2} [inst : TopologicalSpace π] [inst_1 : OrderedRing π] [inst_2 : AddCommMonoid E]
[inst_3 : TopologicalSpace E] [inst_4 : Module π E] {A B : Set E},
IsExposed π A B β B.Nonempty β β l a, B = {x | x β A β§ a β€ l x}
The theorem `IsExposed.eq_inter_halfspace'` states that if `B` is a nonempty set exposed with respect to `A`, then `B` can be represented as the intersection of `A` with some closed halfspace. This is characterized by the existence of a functional `l` and a scalar `a` such that `B` is the set of all elements `x` in `A` where `a` is less than or equal to `l x`. It's important to note that the converse is not true; the corresponding open halfspace not intersecting with `A` doesn't necessarily make `B` an exposed set with respect to `A`.
More concisely: If `B` is a nonempty set exposed with respect to `A` in Lean 4, then there exist a functional `l` and a scalar `a` such that `B` is the set of all `x` in `A` with `a β€ l x`.
|
mem_exposedPoints_iff_exposed_singleton
theorem mem_exposedPoints_iff_exposed_singleton :
β {π : Type u_1} {E : Type u_2} [inst : TopologicalSpace π] [inst_1 : OrderedRing π] [inst_2 : AddCommMonoid E]
[inst_3 : TopologicalSpace E] [inst_4 : Module π E] {A : Set E} {x : E},
x β Set.exposedPoints π A β IsExposed π A {x}
This theorem states that for any topological space 'π', ordered ring 'π', additive commutative monoid 'E', topological space 'E', module 'π E', set 'A' of 'E', and point 'x' in 'E', a point 'x' belongs to the set of exposed points of 'A' if and only if the singleton set containing 'x' is exposed with respect to 'A'. In other words, a point is exposed with respect to a set if and only if there is a hyperplane such that the intersection of the hyperplane with the set is exactly that point, and this is equivalent to the situation where the singleton set containing that point maximizes some functional over the original set.
More concisely: A point x in a topological space E, with respect to a set A in the module E over an ordered ring R and topological space structure, is an exposed point if and held only if the singleton set {x} is an exposed face of A.
|
IsExposed.eq_inter_halfspace
theorem IsExposed.eq_inter_halfspace :
β {π : Type u_1} {E : Type u_2} [inst : TopologicalSpace π] [inst_1 : OrderedRing π] [inst_2 : AddCommMonoid E]
[inst_3 : TopologicalSpace E] [inst_4 : Module π E] [inst_5 : Nontrivial π] {A B : Set E},
IsExposed π A B β β l a, B = {x | x β A β§ a β€ l x}
This theorem states that for a nontrivial ordered ring `π` and for any `E` that forms a module over `π` with a topological space structure, if set `B` is an exposed subset of set `A`, then `B` can be represented as the intersection of `A` with some closed halfspace. In other words, there exists a linear functional `l` and a scalar `a` such that `B` consists of those elements `x` of `A` for which `a` is less than or equal to `l(x)`. Note that the converse of this statement is not true; it would require that the corresponding open halfspace doesn't intersect `A`.
More concisely: For a nontrivial ordered ring `π` and an `π`-module `E` with a topological space structure, any exposed subset `B` of `A` can be represented as the intersection of `A` with a closed halfspace.
|