the Weierstrass theorem

Generalized Weierstrass theorem

theorem IsMinOn.of_isCompact_preimage {E : Type u_1} {F : Type u_2} [CompleteLinearOrder F] [DenselyOrdered F] {f : E → F} [TopologicalSpace E] [TopologicalSpace F] [OrderTopology F] [FirstCountableTopology E] [FirstCountableTopology F] (hf : LowerSemicontinuous f) {y : F} (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) : ∃ (x : E), IsMinOn f Set.univ x

theorem IsCompact_isMinOn_of_isCompact_preimage {E : Type u_1} {F : Type u_2} [CompleteLinearOrder F] [DenselyOrdered F] {f : E → F} [TopologicalSpace E] [TopologicalSpace F] [OrderTopology F] [FirstCountableTopology E] [FirstCountableTopology F] (hf : LowerSemicontinuous f) {y : F} (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) : IsCompact {x : E | IsMinOn f Set.univ x}

Existence of Solutions

def strong_quasi {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [CompleteLinearOrder F] {f : E → F} {𝕜 : Type u_3} [LinearOrderedRing 𝕜] [Module 𝕜 E] : Prop

Equations

• strong_quasi = ∀ ⦃x y : E⦄, x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < max (f x) (f y)

theorem isMinOn_unique {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [CompleteLinearOrder F] {f : E → F} {𝕜 : Type u_3} [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [Module 𝕜 E] (hf' : strong_quasi) {x : E} {y : E} (hx : IsMinOn f Set.univ x) (hy : IsMinOn f Set.univ y) : x = y