Theorem: LowerSemicontinuousWithinAt.sup (Sion/Semicontinuous.lean)

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊔ g x) s a
Tactic:
intro b hb
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊔ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊔ g x) x'

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊔ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊔ g x) x'
Tactic:
simp only [lt_sup_iff] at hb ⊢
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
cases' hb with hb hb
State after:
case inl
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

case inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

State before:
case inl
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
filter_upwards [hf b hb] with x using Or.intro_left _
State after:
no goals

State before:
case inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
filter_upwards [hg b hb] with x using Or.intro_right _
State after:
no goals