Theorem: lowerSemicontinuousWithinAt_iSup₂ (Sion/Semicontinuous.lean)

State before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a
Tactic:
intro t ht
State after:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < (fun x => ⨆ i ∈ I, f i x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'

State before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < (fun x => ⨆ i ∈ I, f i x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
dsimp at ht
State after:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'

State before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
obtain ⟨i, hi, hi'⟩ := hf'.exists_iSup_of_isCompact ne_I hI
State after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
i : ι
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'

State before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
i : ι
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
rw [← hi'] at ht
State after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'

State before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
let h := hf i hi t ht
State after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'

State before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
dsimp
State after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < ⨆ i ∈ I, f i x'

State before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < ⨆ i ∈ I, f i x'
Tactic:
apply Filter.Eventually.mp h
State after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x : α) in 𝓝[s] a, t < f i x → t < ⨆ i ∈ I, f i x

State before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x : α) in 𝓝[s] a, t < f i x → t < ⨆ i ∈ I, f i x
Tactic:
apply Filter.eventually_of_forall
State after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ (x : α), t < f i x → t < ⨆ i ∈ I, f i x

State before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ (x : α), t < f i x → t < ⨆ i ∈ I, f i x
Tactic:
intro x hx
State after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ t < ⨆ i ∈ I, f i x

State before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ t < ⨆ i ∈ I, f i x
Tactic:
apply lt_of_lt_of_le hx
State after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ f i x ≤ ⨆ i ∈ I, f i x

State before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ f i x ≤ ⨆ i ∈ I, f i x
Tactic:
apply le_iSup₂ i hi
State after:
no goals