Theorem: LowerSemicontinuousAt.inf (Sion/Semicontinuous.lean)

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt (fun x => f x ⊓ g x) a
Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊓ g x) univ a

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊓ g x) univ a
Tactic:
exact hf.inf hg
State after:
no goals