Theorem: lowerSemicontinuousOn_iff_restrict (Sion/Semicontinuous.lean)

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ LowerSemicontinuous (restrict s f)
Tactic:
rw [LowerSemicontinuousOn, LowerSemicontinuous, SetCoe.forall]
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔
    ∀ (x : α) (h : x ∈ s), LowerSemicontinuousAt (restrict s f) { val := x, property := h }

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔
    ∀ (x : α) (h : x ∈ s), LowerSemicontinuousAt (restrict s f) { val := x, property := h }
Tactic:
refine' forall₂_congr fun a ha => forall₂_congr fun b _ => _
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : b < f a
⊢ (∀ᶠ (x' : α) in 𝓝[s] a, b < f x') ↔ ∀ᶠ (x' : ↑s) in 𝓝 { val := a, property := ha }, b < restrict s f x'

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : b < f a
⊢ (∀ᶠ (x' : α) in 𝓝[s] a, b < f x') ↔ ∀ᶠ (x' : ↑s) in 𝓝 { val := a, property := ha }, b < restrict s f x'
Tactic:
simp only [nhdsWithin_eq_map_subtype_coe ha, eventually_map, restrict]
State after:
no goals