Theorem: LowerSemicontinuousWithinAt.inf (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_inf_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:
exact Eventually.and (hf b hb.1) (hg b hb.2)
State after:
no goals