Theorems · Theorem · optimization

Sion.exists_lt_iInf_of_lt_iInf_of_finite

∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F],
                    Convex ℝ X →
                      ∀ {s : Set F},
                        s.Finite → s ⊆ Y → ∀ {t : β}, (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Defined in

Mathlib.Topology.Sion

Cited by

1 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderTopologicalSpaceAddCommGroupModuleIsTopologicalAddGroupContinuousSMulTopologicalSpaceAddCommGroupModuleDenselyOrderedIsTopologicalAddGroupContinuousSMul