case inl
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x

case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
intro y hy
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
no goals
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.113012
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type ?u.113041
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
filter_upwards [h i y hi, bdd]with y hy hy' using hy.trans_le (le_ciSup hy' i)