Set.Nonempty.intrinsicClosure
theorem Set.Nonempty.intrinsicClosure :
∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
[inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P},
s.Nonempty → (intrinsicClosure 𝕜 s).Nonempty
This theorem, referred to as an **Alias** of the reverse direction of `intrinsicClosure_nonempty`, states that for any nonempty set `s` in an affine torsor `P` over a topological vector space `V` with scalars in a ring `𝕜`, the intrinsic closure of `s` is also nonempty. Essentially, it asserts that if a set has at least one element, then its intrinsic closure, which is the closure of `s` considered as a set in its affine span, will also contain at least one element.
More concisely: If `s` is a nonempty subset of an affine torsor over a topological vector space with scalars in a ring, then the intrinsic closure of `s` is a nonempty set.
|
Set.Nonempty.ofIntrinsicClosure
theorem Set.Nonempty.ofIntrinsicClosure :
∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
[inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P},
(intrinsicClosure 𝕜 s).Nonempty → s.Nonempty
This theorem, known as an **Alias** of the forward direction of `intrinsicClosure_nonempty`, states that for any types 𝕜, V and P, where 𝕜 is a ring, V is an additive commutative group, 𝕜 is a module over V, P is a topological space, and V is an additive torsor over P, if a set `s` of type P has a nonempty intrinsic closure, then the set `s` itself is nonempty. The intrinsic closure of a set is defined as its closure in the affine span considered as a set. This theorem essentially says that you cannot get a nonempty intrinsic closure from an empty set.
More concisely: If a set in a topological space has a nonempty intrinsic closure as an additive torsor over a ring and a commutative additive group, then the set itself is nonempty.
|
Set.Nonempty.intrinsicInterior
theorem Set.Nonempty.intrinsicInterior :
∀ {V : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{s : Set V}, Convex ℝ s → s.Nonempty → (intrinsicInterior ℝ s).Nonempty
This theorem states that for any non-empty convex set `s` in a real finite-dimensional normed vector space `V`, the intrinsic interior of `s` is also non-empty. In other words, if we have a set of vectors that forms a convex space (meaning, the line segment between any two points in the set stays within the set), and if this set is not empty, then the intrinsic interior of this set, which is the interior of the set when considered within its affine span, is likewise non-empty.
More concisely: In a finite-dimensional real normed vector space, every non-empty convex set has a non-empty intrinsic interior within its affine span.
|