ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : y ≤ 0<GOAL>LowerSemicontinuousOn (s.indicator fun _x => y) t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : y ≤ 0<GOAL>LowerSemicontinuousAt (s.indicator fun _x => y) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : y ≤ 0<GOAL>LowerSemicontinuousWithinAt (s.indicator fun _x => y) t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<GOAL>LowerSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Ioi y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>hf : LowerSemicontinuous f<VAR>y : β<GOAL>IsOpen (f ⁻¹' Set.Ioi y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>f : α → γ<GOAL>LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Iic y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>f : α → γ<VAR>hf : LowerSemicontinuous f<VAR>y : γ<GOAL>IsClosed (f ⁻¹' Set.Iic y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousWithinAt f s x<GOAL>LowerSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousAt f x<GOAL>LowerSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousOn f s<GOAL>LowerSemicontinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : Continuous f<GOAL>LowerSemicontinuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (𝓝[s] x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuousAt f x ↔ f x ≤ Filter.liminf f (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ Filter.liminf f (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ Filter.liminf f (𝓝[s] x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>LowerSemicontinuous f ↔ IsClosed {p | f p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>gmon : Monotone g<GOAL>LowerSemicontinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : LowerSemicontinuousAt f x<VAR>gmon : Monotone g<GOAL>LowerSemicontinuousAt (g ∘ f) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : LowerSemicontinuousOn f s<VAR>gmon : Monotone g<GOAL>LowerSemicontinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : LowerSemicontinuous f<VAR>gmon : Monotone g<GOAL>LowerSemicontinuous (g ∘ f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>gmon : Antitone g<GOAL>UpperSemicontinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : LowerSemicontinuousAt f x<VAR>gmon : Antitone g<GOAL>UpperSemicontinuousAt (g ∘ f) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : LowerSemicontinuousOn f s<VAR>gmon : Antitone g<GOAL>UpperSemicontinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : LowerSemicontinuous f<VAR>gmon : Antitone g<GOAL>UpperSemicontinuous (g ∘ f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>x : ι<VAR>hf : LowerSemicontinuousAt f (g x)<VAR>hg : ContinuousAt g x<GOAL>LowerSemicontinuousAt (fun x => f (g x)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>y : α<VAR>x : ι<VAR>hf : LowerSemicontinuousAt f y<VAR>hg : ContinuousAt g x<VAR>hy : g x = y<GOAL>LowerSemicontinuousAt (fun x => f (g x)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>hf : LowerSemicontinuous f<VAR>hg : Continuous g<GOAL>LowerSemicontinuous fun x => f (g x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>hg : LowerSemicontinuousWithinAt g s x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>LowerSemicontinuousWithinAt (fun z => f z + g z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousAt f x<VAR>hg : LowerSemicontinuousAt g x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>LowerSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousOn f s<VAR>hg : LowerSemicontinuousOn g s<VAR>hcont : ∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>LowerSemicontinuousOn (fun z => f z + g z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuous f<VAR>hg : LowerSemicontinuous g<VAR>hcont : ∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>LowerSemicontinuous fun z => f z + g z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>hg : LowerSemicontinuousWithinAt g s x<GOAL>LowerSemicontinuousWithinAt (fun z => f z + g z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousAt f x<VAR>hg : LowerSemicontinuousAt g x<GOAL>LowerSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousOn f s<VAR>hg : LowerSemicontinuousOn g s<GOAL>LowerSemicontinuousOn (fun z => f z + g z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuous f<VAR>hg : LowerSemicontinuous g<GOAL>LowerSemicontinuous fun z => f z + g z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s<GOAL>LowerSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuous (f i)<GOAL>LowerSemicontinuous fun z => ∑ i ∈ a, f i z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (Set.range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), LowerSemicontinuousWithinAt (f i hi) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (Set.range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), LowerSemicontinuousAt (f i hi) x<GOAL>LowerSemicontinuousAt (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ x ∈ s, BddAbove (Set.range fun i => f i x)<VAR>h : ∀ (i : ι), LowerSemicontinuousOn (f i) s<GOAL>LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), LowerSemicontinuousOn (f i) s<GOAL>LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), LowerSemicontinuousOn (f i hi) s<GOAL>LowerSemicontinuousOn (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ (x : α), BddAbove (Set.range fun i => f i x)<VAR>h : ∀ (i : ι), LowerSemicontinuous (f i)<GOAL>LowerSemicontinuous fun x' => ⨆ i, f i x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), LowerSemicontinuous (f i)<GOAL>LowerSemicontinuous fun x' => ⨆ i, f i x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), LowerSemicontinuous (f i hi)<GOAL>LowerSemicontinuous fun x' => ⨆ i, ⨆ (hi : p i), f i hi x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousOn (f i) s<GOAL>LowerSemicontinuousOn (fun x' => ∑' (i : ι), f i x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuous (f i)<GOAL>LowerSemicontinuous fun x' => ∑' (i : ι), f i x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s t : Set α<VAR>h : UpperSemicontinuousWithinAt f s x<VAR>hst : t ⊆ s<GOAL>UpperSemicontinuousWithinAt f t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<GOAL>UpperSemicontinuousWithinAt f Set.univ x ↔ UpperSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : UpperSemicontinuousAt f x<GOAL>UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : UpperSemicontinuousOn f s<VAR>hx : x ∈ s<GOAL>UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>h : UpperSemicontinuousOn f s<VAR>hst : t ⊆ s<GOAL>UpperSemicontinuousOn f t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<GOAL>UpperSemicontinuousOn f Set.univ ↔ UpperSemicontinuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : UpperSemicontinuous f<VAR>x : α<GOAL>UpperSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : UpperSemicontinuous f<VAR>s : Set α<VAR>x : α<GOAL>UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : UpperSemicontinuous f<VAR>s : Set α<GOAL>UpperSemicontinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>z : β<GOAL>UpperSemicontinuousWithinAt (fun _x => z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>z : β<GOAL>UpperSemicontinuousAt (fun _x => z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>z : β<GOAL>UpperSemicontinuousOn (fun _x => z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>z : β<GOAL>UpperSemicontinuous fun _x => z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : y ≤ 0<GOAL>UpperSemicontinuous (s.indicator fun _x => y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : y ≤ 0<GOAL>UpperSemicontinuousOn (s.indicator fun _x => y) t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : y ≤ 0<GOAL>UpperSemicontinuousAt (s.indicator fun _x => y) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : y ≤ 0<GOAL>UpperSemicontinuousWithinAt (s.indicator fun _x => y) t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : 0 ≤ y<GOAL>UpperSemicontinuous (s.indicator fun _x => y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : 0 ≤ y<GOAL>UpperSemicontinuousOn (s.indicator fun _x => y) t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : 0 ≤ y<GOAL>UpperSemicontinuousAt (s.indicator fun _x => y) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : 0 ≤ y<GOAL>UpperSemicontinuousWithinAt (s.indicator fun _x => y) t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<GOAL>UpperSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Iio y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>hf : UpperSemicontinuous f<VAR>y : β<GOAL>IsOpen (f ⁻¹' Set.Iio y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>f : α → γ<GOAL>UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Ici y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>f : α → γ<VAR>hf : UpperSemicontinuous f<VAR>y : γ<GOAL>IsClosed (f ⁻¹' Set.Ici y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousWithinAt f s x<GOAL>UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousAt f x<GOAL>UpperSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : ContinuousOn f s<GOAL>UpperSemicontinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<VAR>h : Continuous f<GOAL>UpperSemicontinuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>UpperSemicontinuousWithinAt f s x ↔ Filter.limsup f (𝓝[s] x) ≤ f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>UpperSemicontinuousAt f x ↔ Filter.limsup f (𝓝 x) ≤ f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>UpperSemicontinuous f ↔ ∀ (x : α), Filter.limsup f (𝓝 x) ≤ f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>f : α → γ<GOAL>UpperSemicontinuousOn f s ↔ ∀ x ∈ s, Filter.limsup f (𝓝[s] x) ≤ f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>CompleteLinearOrder γ<VAR>DenselyOrdered γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>UpperSemicontinuous f ↔ IsClosed {p | p.2 ≤ f p.1}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : UpperSemicontinuousWithinAt f s x<VAR>gmon : Monotone g<GOAL>UpperSemicontinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : UpperSemicontinuousAt f x<VAR>gmon : Monotone g<GOAL>UpperSemicontinuousAt (g ∘ f) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : UpperSemicontinuousOn f s<VAR>gmon : Monotone g<GOAL>UpperSemicontinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : UpperSemicontinuous f<VAR>gmon : Monotone g<GOAL>UpperSemicontinuous (g ∘ f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : UpperSemicontinuousWithinAt f s x<VAR>gmon : Antitone g<GOAL>LowerSemicontinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : ContinuousAt g (f x)<VAR>hf : UpperSemicontinuousAt f x<VAR>gmon : Antitone g<GOAL>LowerSemicontinuousAt (g ∘ f) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : UpperSemicontinuousOn f s<VAR>gmon : Antitone g<GOAL>LowerSemicontinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>δ : Type u_4<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderTopology δ<VAR>g : γ → δ<VAR>f : α → γ<VAR>hg : Continuous g<VAR>hf : UpperSemicontinuous f<VAR>gmon : Antitone g<GOAL>LowerSemicontinuous (g ∘ f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>x : ι<VAR>hf : UpperSemicontinuousAt f (g x)<VAR>hg : ContinuousAt g x<GOAL>UpperSemicontinuousAt (fun x => f (g x)) x