α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
hz : z < indicator s (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
⊢ LowerSemicontinuous (indicator s fun _x => y)
intro x z hz
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'

case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : ¬x ∈ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
hz : z < indicator s (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
by_cases h : x ∈ s <;> simp [h] at hz
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ (a : α), a ∈ s → z < indicator s (fun _x => y) a
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
filter_upwards [hs.mem_nhds h]
no goals
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ (a : α), a ∈ s → z < indicator s (fun _x => y) a
simp (config := { contextual := true }) [hz]
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : ¬x ∈ s
hz : z < 0
x' : α
⊢ z < indicator s (fun _x => y) x'
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : ¬x ∈ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
refine Filter.eventually_of_forall fun x' => ?_
no goals
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsOpen s
hy : 0 ≤ y
x : α
z : β
h : ¬x ∈ s
hz : z < 0
x' : α
⊢ z < indicator s (fun _x => y) x'
by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]