LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Strict

`StrictConvex.preimage_add_right` theorem StrictConvex.preimage_add_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCancelCommMonoid E] [inst_3 : ContinuousAdd E] [inst_4 : Module 𝕜 E] {s : Set E}, StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s) The theorem `StrictConvex.preimage_add_right` states that for any ordered semiring `𝕜` and topological space `E` that also has the structure of an additive cancelable commutative monoid, a module over `𝕜`, and supports continuous addition, if a set `s` in `E` is strictly convex, then the translation of the set `s` by any element `z` in `E` is also strictly convex. Translation of a set by an element means that each element in the set is added with `z`. Strict convexity, in this context, means that for any two distinct points in the set, the open line segment that connects them lies entirely in the interior of the set. More concisely: If `s` is a strictly convex subset of an additive cancelable commutative monoid `E` in a topological space, then for any `z` in `E`, the translated set `s + z` is also strictly convex.
`strictConvex_iff_convex` theorem strictConvex_iff_convex : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {s : Set 𝕜}, StrictConvex 𝕜 s ↔ Convex 𝕜 s The theorem `strictConvex_iff_convex` states that for any set `s` in a linear ordered field `𝕜`, which has a topology and an order topology, the set `s` is strictly convex if and only if it is convex. In other words, a set is strictly convex, meaning the open segment between any two distinct points lies in its interior, if and only if it is convex, meaning it is star-shaped around any point in the set. More concisely: A set in a linear ordered field with a topology and an order topology is strictly convex if and only if it is convex.
`StrictConvex.ordConnected` theorem StrictConvex.ordConnected : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {s : Set 𝕜}, StrictConvex 𝕜 s → s.OrdConnected This theorem, called `StrictConvex.ordConnected`, asserts that for a given set `s` of a particular type `𝕜`, if the set `s` is strictly convex, then it is also ordinally connected. Here, 'strictly convex' means that the open segment between any two distinct points in the set lies in its interior, implying that the set is convex and not flat on the boundary. 'Ordinally connected' means that for any two points in the set, all points between them (with respect to the order on `𝕜`) are also in the set. The type `𝕜` is assumed to be a linearly ordered field and a topological space with an order topology. More concisely: If a strictly convex set in a linearly ordered field and topological space is given, then it is ordinally connected.
`StrictConvex.affine_preimage` theorem StrictConvex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : OrderedRing 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : TopologicalSpace F] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] {s : Set F}, StrictConvex 𝕜 s → ∀ {f : E →ᵃ[𝕜] F}, Continuous ⇑f → Function.Injective ⇑f → StrictConvex 𝕜 (⇑f ⁻¹' s) The theorem states that for any strictly convex set 's' in a topological vector space 'F' over an ordered ring '𝕜', the preimage of 's' under a continuous and injective affine transformation 'f' from another topological vector space 'E' over '𝕜' is also strictly convex. In other words, if a set is strictly convex and we apply an affine transformation, then the set of points that get mapped into this strictly convex set by 'f' is also strictly convex. More concisely: Given a strictly convex set 's' in a topological vector space 'F' over an ordered ring '𝕜', and a continuous, injective affine transformation 'f' from another topological vector space 'E' to 'F', the preimage of 's' under 'f' is strictly convex.
`Convex.strictConvex_of_isOpen` theorem Convex.strictConvex_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] {s : Set E}, IsOpen s → Convex 𝕜 s → StrictConvex 𝕜 s The theorem `Convex.strictConvex_of_isOpen` states that, for any open set `s` in a topological space `E` over a certain ordered semiring `𝕜`, if `s` is convex, then it is also strictly convex. In other words, if `s` is an open set and every point inside `s` is a convex combination of any other two points in `s`, then the open line segment between any two distinct points in `s` lies entirely in the interior of `s`, ensuring that `s` is not "flat" on its boundary. More concisely: If `s` is an open and convex subset of a topological space over an ordered semiring, then every line segment between any two distinct points in `s` lies entirely in the interior of `s`.
`StrictConvex.affine_image` theorem StrictConvex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : OrderedRing 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : TopologicalSpace F] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] {s : Set E}, StrictConvex 𝕜 s → ∀ {f : E →ᵃ[𝕜] F}, IsOpenMap ⇑f → StrictConvex 𝕜 (⇑f '' s) The theorem `StrictConvex.affine_image` states that if we have a strictly convex set in a given topological space, then the image of this set under any affine map that is an open map will also be strictly convex. Here, a set is strictly convex if the open line segment between any two distinct points in the set is entirely contained within the set. An affine map is a function that preserves collinearity (i.e., all points lying on the same line initially will still be on the same line after the transformation) and ratios of distances (e.g., the midpoint of a line segment remains the midpoint after the transformation). An open map is a function that maps open sets to open sets. The types `𝕜`, `E`, and `F` represent the type of scalars and the types of the initial and target topological spaces respectively. More concisely: If `S` is a strictly convex subset of a topological space `E` and `f : E → F` is an open, affine map, then `f(S)` is a strictly convex subset of `F`.
`Set.OrdConnected.strictConvex` theorem Set.OrdConnected.strictConvex : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : OrderedSemiring 𝕜] [inst_1 : TopologicalSpace β] [inst_2 : LinearOrderedCancelAddCommMonoid β] [inst_3 : OrderTopology β] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set β}, s.OrdConnected → StrictConvex 𝕜 s This theorem states that for any ordered semiring `𝕜` and any type `β` that is a topological space, a linearly ordered cancellative additive commutative monoid, has an order topology, is a module over `𝕜`, and has a scalar multiplication that respects the order, if a set `s` of `β` is order-connected, then `s` is strictly convex in `𝕜`. In other words, if `s` has the property that for any two points in `s`, all points between those two are also in `s`, then `s` is strictly convex meaning that the open line segment between any two distinct points in `s` is contained in the interior of `s`. More concisely: Given an ordered semiring `𝕜`, a topological space `β` that is a linearly ordered cancellative additive commutative monoid with an order topology, a `𝕜`-module structure, and respects the order, if `s` is an order-connected subset of `β`, then `s` is strictly convex.
`StrictConvex.vadd` theorem StrictConvex.vadd : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : ContinuousAdd E] {s : Set E}, StrictConvex 𝕜 s → ∀ (x : E), StrictConvex 𝕜 (x +ᵥ s) The theorem `StrictConvex.vadd` states that for any strictly convex set `s` in a topological vector space `E` over an ordered semiring `𝕜`, the translation of `s` by any vector `x` in `E` is also a strictly convex set. In other words, if `s` is strictly convex, then so is the set obtained by adding `x` to every point in `s`. Here, a set is defined to be strictly convex if, for any two distinct points in the set, the open segment between them (excluding the endpoints) lies entirely within the set. More concisely: If `s` is a strictly convex set in a topological vector space over an ordered semiring, then the translated set `s + x` is also strictly convex for any vector `x` in the space.
`strictConvex_iff_div` theorem strictConvex_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] {s : Set E}, StrictConvex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s This theorem provides an alternative definition of strict convexity for a set in a vector space. A set `s` is strictly convex in a vector space `E` over a linearly ordered field `𝕜` if and only if for every pair of distinct points `x` and `y` in `s`, for any `a` and `b` in `𝕜` with `a` and `b` greater than zero, the point obtained by taking the weighted average of `x` and `y` with weights `a / (a + b)` and `b / (a + b)` respectively, is in the interior of `s`. This definition characterizes strict convexity in terms of the interior of the set and the division operation. More concisely: A set in a vector space is strictly convex if and only if for any distinct points in the set, their weighted average with positive weights lies in the set's interior.
`StrictConvex.preimage_add_left` theorem StrictConvex.preimage_add_left : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCancelCommMonoid E] [inst_3 : ContinuousAdd E] [inst_4 : Module 𝕜 E] {s : Set E}, StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s) The theorem `StrictConvex.preimage_add_left` states that for any strictly convex set, a translation of the set results in another strictly convex set. More precisely, if we have a strictly convex set `s` in a topological space `E` over an ordered semiring `𝕜`, then for any element `z` in `E`, the set obtained by translating each element of `s` by `z` (mathematically, this is the preimage of the function `x => x + z`) is also strictly convex. The conditions that `𝕜` is an ordered semiring, `E` is a topological space with a 'continuous add' operation and forms a module over `𝕜`, ensure the mathematical soundness of the operations involved in the statement. More concisely: If `s` is a strictly convex set in a topological space `E` over an ordered semiring `𝕜`, then the translation of `s` by any element `z` in `E` is also strictly convex.