LeanPool.SardMoreira.UpperLowerSemicontinuous

theorem Topology.continuousWithinAt_toLower_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {s : Set X} {x : X} : ContinuousWithinAt (⇑WithLower.toLower ∘ f) s x ↔ UpperSemicontinuousWithinAt f s x

theorem Topology.continuousWithinAt_toUpper_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {s : Set X} {x : X} : ContinuousWithinAt (⇑WithUpper.toUpper ∘ f) s x ↔ LowerSemicontinuousWithinAt f s x

theorem Topology.continuousAt_toLower_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {x : X} : ContinuousAt (⇑WithLower.toLower ∘ f) x ↔ UpperSemicontinuousAt f x

theorem Topology.continuousAt_toUpper_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {x : X} : ContinuousAt (⇑WithUpper.toUpper ∘ f) x ↔ LowerSemicontinuousAt f x

theorem Topology.continuousOn_toLower_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {s : Set X} : ContinuousOn (⇑WithLower.toLower ∘ f) s ↔ UpperSemicontinuousOn f s

theorem Topology.continuousOn_toUpper_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} {s : Set X} : ContinuousOn (⇑WithUpper.toUpper ∘ f) s ↔ LowerSemicontinuousOn f s

theorem Topology.continuous_toLower_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} : Continuous (⇑WithLower.toLower ∘ f) ↔ UpperSemicontinuous f

theorem Topology.continuous_toUpper_comp_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder Y] {f : X → Y} : Continuous (⇑WithUpper.toUpper ∘ f) ↔ LowerSemicontinuous f

theorem LowerSemicontinuousOn.exists_isMinOn' {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [LinearOrder α] {f : X → α} {s : Set X} (hf : LowerSemicontinuousOn f s) (hs : IsCompact s) (hne : s.Nonempty) : ∃ x ∈ s, IsMinOn f s x