[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x
[PROOFSTEP]
simp [LowerSemicontinuousWithinAt, LowerSemicontinuousAt, nhdsWithin_univ]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f
[PROOFSTEP]
simp [LowerSemicontinuousOn, LowerSemicontinuous, lowerSemicontinuousWithinAt_univ_iff]
[GOAL]
α : 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)
[PROOFSTEP]
intro x z hz
[GOAL]
α : 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'
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
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 : β
hz : z < indicator s (fun _x => y) x
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h] at hz
[GOAL]
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 : β
hz : z < indicator s (fun _x => y) x
h : ¬x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h] at hz
[GOAL]
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'
[PROOFSTEP]
filter_upwards [hs.mem_nhds h]
[GOAL]
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
[PROOFSTEP]
simp (config := { contextual := true }) [hz]
[GOAL]
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'
[PROOFSTEP]
refine Filter.eventually_of_forall fun x' => ?_
[GOAL]
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'
[PROOFSTEP]
by_cases h' : x' ∈ s
[GOAL]
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 < 0
x' : α
h' : x' ∈ s
⊢ z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h', hz.trans_le hy, hz]
[GOAL]
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' : α
h' : ¬x' ∈ s
⊢ z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h', hz.trans_le hy, hz]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
⊢ LowerSemicontinuous (indicator s fun _x => y)
[PROOFSTEP]
intro x z hz
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
hz : z < indicator s (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
hz : z < indicator s (fun _x => y) x
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h] at hz
[GOAL]
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
hz : z < indicator s (fun _x => y) x
h : ¬x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h] at hz
[GOAL]
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
refine Filter.eventually_of_forall fun x' => ?_
[GOAL]
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
⊢ z < indicator s (fun _x => y) x'
[PROOFSTEP]
by_cases h' : x' ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∈ s
⊢ z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h', hz, hz.trans_le hy]
[GOAL]
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : ¬x' ∈ s
⊢ z < indicator s (fun _x => y) x'
[PROOFSTEP]
simp [h', hz, hz.trans_le hy]
[GOAL]
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : ¬x ∈ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < indicator s (fun _x => y) x'
[PROOFSTEP]
filter_upwards [hs.isOpen_compl.mem_nhds h]
[GOAL]
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f g : α → β
x✝ : α
s t : Set α
y z✝ : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : ¬x ∈ s
hz : z < 0
⊢ ∀ (a : α), a ∈ sᶜ → z < indicator s (fun _x => y) a
[PROOFSTEP]
simp (config := { contextual := true }) [hz]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)
[PROOFSTEP]
rw [lowerSemicontinuous_iff_isOpen_preimage]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)
[PROOFSTEP]
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]
[GOAL]
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'
[PROOFSTEP]
by_cases h : ∃ l, l < f x
[GOAL]
case pos
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'
[PROOFSTEP]
obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y := exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'
[PROOFSTEP]
filter_upwards [hf z zlt] with a ha
[GOAL]
case h
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : z < f a
⊢ y < (g ∘ f) a
[PROOFSTEP]
calc
  y < g (min (f x) (f a)) := hz (by simp [zlt, ha, le_refl])
  _ ≤ g (f a) := gmon (min_le_right _ _)
[GOAL]
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : z < f a
⊢ min (f x) (f a) ∈ Ioc z (f x)
[PROOFSTEP]
simp [zlt, ha, le_refl]
[GOAL]
case neg
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'
[PROOFSTEP]
simp only [not_exists, not_lt] at h
[GOAL]
case neg
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∀ (x_1 : γ), f x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'
[PROOFSTEP]
exact Filter.eventually_of_forall fun a => hy.trans_le (gmon (h (f a)))
[GOAL]
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x
[PROOFSTEP]
simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
[GOAL]
α : Type u_1
inst✝⁷ : TopologicalSpace α
β : Type u_2
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x
[PROOFSTEP]
exact hg.comp_lowerSemicontinuousWithinAt hf gmon
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
⊢ LowerSemicontinuousWithinAt (fun z => f z + g z) s x
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
  ∃ u v : Set γ, IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ {p : γ × γ | y < p.fst + p.snd} :=
  mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
by_cases hx₁ : ∃ l, l < f x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u := exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
by_cases hx₂ : ∃ l, l < g x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v := exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
⊢ y < f z + g z
[PROOFSTEP]
have A1 : min (f z) (f x) ∈ u := by
  by_cases H : f z ≤ f x
  · simp [H]
    exact h₁ ⟨h₁z, H⟩
  · simp [le_of_not_le H]
    exact h₁ ⟨z₁lt, le_rfl⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
by_cases H : f z ≤ f x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
H : f z ≤ f x
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
simp [H]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
H : f z ≤ f x
⊢ f z ∈ u
[PROOFSTEP]
exact h₁ ⟨h₁z, H⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
H : ¬f z ≤ f x
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
simp [le_of_not_le H]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
H : ¬f z ≤ f x
⊢ f x ∈ u
[PROOFSTEP]
exact h₁ ⟨z₁lt, le_rfl⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
⊢ y < f z + g z
[PROOFSTEP]
have A2 : min (g z) (g x) ∈ v := by
  by_cases H : g z ≤ g x
  · simp [H]
    exact h₂ ⟨h₂z, H⟩
  · simp [le_of_not_le H]
    exact h₂ ⟨z₂lt, le_rfl⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
by_cases H : g z ≤ g x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
simp [H]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
H : g z ≤ g x
⊢ g z ∈ v
[PROOFSTEP]
exact h₂ ⟨h₂z, H⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
H : ¬g z ≤ g x
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
simp [le_of_not_le H]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
H : ¬g z ≤ g x
⊢ g x ∈ v
[PROOFSTEP]
exact h₂ ⟨z₂lt, le_rfl⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
A2 : min (g z) (g x) ∈ v
⊢ y < f z + g z
[PROOFSTEP]
have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : z₁ < f z
h₂z : z₂ < g z
A1 : min (f z) (f x) ∈ u
A2 : min (g z) (g x) ∈ v
this : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v
⊢ y < f z + g z
[PROOFSTEP]
calc
  y < min (f z) (f x) + min (g z) (g x) := h this
  _ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
simp only [not_exists, not_lt] at hx₂
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
filter_upwards [hf z₁ z₁lt] with z h₁z
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
⊢ y < f z + g z
[PROOFSTEP]
have A1 : min (f z) (f x) ∈ u := by
  by_cases H : f z ≤ f x
  · simp [H]
    exact h₁ ⟨h₁z, H⟩
  · simp [le_of_not_le H]
    exact h₁ ⟨z₁lt, le_rfl⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
by_cases H : f z ≤ f x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
H : f z ≤ f x
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
simp [H]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
H : f z ≤ f x
⊢ f z ∈ u
[PROOFSTEP]
exact h₁ ⟨h₁z, H⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
H : ¬f z ≤ f x
⊢ min (f z) (f x) ∈ u
[PROOFSTEP]
simp [le_of_not_le H]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
H : ¬f z ≤ f x
⊢ f x ∈ u
[PROOFSTEP]
exact h₁ ⟨z₁lt, le_rfl⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
A1 : min (f z) (f x) ∈ u
⊢ y < f z + g z
[PROOFSTEP]
have : (min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : z₁ < f z
A1 : min (f z) (f x) ∈ u
this : (min (f z) (f x), g x) ∈ u ×ˢ v
⊢ y < f z + g z
[PROOFSTEP]
calc
  y < min (f z) (f x) + g x := h this
  _ ≤ f z + g z := add_le_add (min_le_left _ _) (hx₂ (g z))
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
simp only [not_exists, not_lt] at hx₁
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
by_cases hx₂ : ∃ l, l < g x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v := exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
filter_upwards [hg z₂ z₂lt] with z h₂z
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
⊢ y < f z + g z
[PROOFSTEP]
have A2 : min (g z) (g x) ∈ v := by
  by_cases H : g z ≤ g x
  · simp [H]
    exact h₂ ⟨h₂z, H⟩
  · simp [le_of_not_le H]
    exact h₂ ⟨z₂lt, le_rfl⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
by_cases H : g z ≤ g x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
simp [H]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
H : g z ≤ g x
⊢ g z ∈ v
[PROOFSTEP]
exact h₂ ⟨h₂z, H⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
H : ¬g z ≤ g x
⊢ min (g z) (g x) ∈ v
[PROOFSTEP]
simp [le_of_not_le H]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
H : ¬g z ≤ g x
⊢ g x ∈ v
[PROOFSTEP]
exact h₂ ⟨z₂lt, le_rfl⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
A2 : min (g z) (g x) ∈ v
⊢ y < f z + g z
[PROOFSTEP]
have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : z₂ < g z
A2 : min (g z) (g x) ∈ v
this : (f x, min (g z) (g x)) ∈ u ×ˢ v
⊢ y < f z + g z
[PROOFSTEP]
calc
  y < f x + min (g z) (g x) := h this
  _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
simp only [not_exists, not_lt] at hx₁ hx₂
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
[PROOFSTEP]
apply Filter.eventually_of_forall
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ (x : α), y < (fun z => f z + g z) x
[PROOFSTEP]
intro z
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
⊢ y < (fun z => f z + g z) z
[PROOFSTEP]
have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
y : γ
hy : y < (fun z => f z + g z) x
u v : Set γ
u_open : IsOpen u
xu : f x ∈ u
v_open : IsOpen v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.fst + p.snd}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
this : (f x, g x) ∈ u ×ˢ v
⊢ y < (fun z => f z + g z) z
[PROOFSTEP]
calc
  y < f x + g x := h this
  _ ≤ f z + g z := add_le_add (hx₁ (f z)) (hx₂ (g z))
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousAt f x
hg : LowerSemicontinuousAt g x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
⊢ LowerSemicontinuousAt (fun z => f z + g z) x
[PROOFSTEP]
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt (fun z => f z + g z) univ x
[PROOFSTEP]
exact hf.add' hg hcont
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
[PROOFSTEP]
classical
induction' a using Finset.induction_on with i a ia IH
· exact lowerSemicontinuousWithinAt_const
· simp only [ia, Finset.sum_insert, not_false_iff]
  exact
    LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self i a))
      (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
[PROOFSTEP]
induction' a using Finset.induction_on with i a ia IH
[GOAL]
case empty
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha✝ : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
ha : ∀ (i : ι), i ∈ ∅ → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in ∅, f i z) s x
[PROOFSTEP]
exact lowerSemicontinuousWithinAt_const
[GOAL]
case insert
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in insert i a, f i z) s x
[PROOFSTEP]
simp only [ia, Finset.sum_insert, not_false_iff]
[GOAL]
case insert
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => f i z + ∑ i in a, f i z) s x
[PROOFSTEP]
exact
  LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self i a))
    (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun z => ∑ i in a, f i z) x
[PROOFSTEP]
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) univ x
[PROOFSTEP]
exact lowerSemicontinuousWithinAt_sum ha
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
[PROOFSTEP]
simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const
[GOAL]
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
[PROOFSTEP]
intro y hy
[GOAL]
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
[PROOFSTEP]
rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
[GOAL]
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y✝ z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ (i : ι), f i x') x
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ (i : ι), f i x') x'
[PROOFSTEP]
filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ⨆ (i : ι), f i x') x
[PROOFSTEP]
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
[PROOFSTEP]
rw [← nhdsWithin_univ] at bdd
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
[PROOFSTEP]
exact lowerSemicontinuousWithinAt_ciSup bdd h
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousOn (f i) s
⊢ ∀ (x : α), x ∈ s → BddAbove (range fun i => f i x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type u_2
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_4
δ' : Type u_5
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuous (f i)
⊢ ∀ (x : α), BddAbove (range fun i => f i x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
[PROOFSTEP]
simp_rw [ENNReal.tsum_eq_iSup_sum]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (s : Finset ι), ∑ i in s, f i x') s x
[PROOFSTEP]
refine lowerSemicontinuousWithinAt_iSup fun b => ?_
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' => ∑ i in b, f i x') s x
[PROOFSTEP]
exact lowerSemicontinuousWithinAt_sum fun i _hi => h i
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
[PROOFSTEP]
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x
[PROOFSTEP]
exact lowerSemicontinuousWithinAt_tsum h
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x
[PROOFSTEP]
simp [UpperSemicontinuousWithinAt, UpperSemicontinuousAt, nhdsWithin_univ]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f
[PROOFSTEP]
simp [UpperSemicontinuousOn, UpperSemicontinuous, upperSemicontinuousWithinAt_univ_iff]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)
[PROOFSTEP]
rw [upperSemicontinuous_iff_isOpen_preimage]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)
[PROOFSTEP]
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
⊢ UpperSemicontinuousAt (fun z => f z + g z) x
[PROOFSTEP]
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z => f z + g z) univ x
[PROOFSTEP]
exact hf.add' hg hcont
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt (fun z => ∑ i in a, f i z) x
[PROOFSTEP]
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
β : Type u_2
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt (fun z => ∑ i in a, f i z) univ x
[PROOFSTEP]
exact upperSemicontinuousWithinAt_sum ha
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
[PROOFSTEP]
refine' ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, _⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
intro v hv
[GOAL]
case intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ v ∈ map f (𝓝[s] x)
[PROOFSTEP]
simp only [Filter.mem_map]
[GOAL]
case intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
by_cases Hl : ∃ l, l < f x
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
by_cases Hu : ∃ u, f x < u
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
⊢ a ∈ f ⁻¹' v
[PROOFSTEP]
cases' le_or_gt (f a) (f x) with h h
[GOAL]
case h.inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v
[PROOFSTEP]
exact hl ⟨lfa, h⟩
[GOAL]
case h.inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
h : f a > f x
⊢ a ∈ f ⁻¹' v
[PROOFSTEP]
exact hu ⟨le_of_lt h, fau⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ¬∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
simp only [not_exists, not_lt] at Hu
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (x_1 : γ), x_1 ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ¬∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
simp only [not_exists, not_lt] at Hl
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
by_cases Hu : ∃ u, f x < u
[GOAL]
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
filter_upwards [h₂ u fxu] with a lfa
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ a ∈ f ⁻¹' v
[PROOFSTEP]
apply hu
[GOAL]
case h.a
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ f a ∈ Ico (f x) u
[PROOFSTEP]
exact ⟨Hl (f a), lfa⟩
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ¬∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
simp only [not_exists, not_lt] at Hu
[GOAL]
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
[PROOFSTEP]
apply Filter.eventually_of_forall
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
⊢ ∀ (x : α), f x ∈ v
[PROOFSTEP]
intro a
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
a : α
⊢ f a ∈ v
[PROOFSTEP]
have : f a = f x := le_antisymm (Hu _) (Hl _)
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
a : α
this : f a = f x
⊢ f a ∈ v
[PROOFSTEP]
rw [this]
[GOAL]
case neg.hp
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
a : α
this : f a = f x
⊢ f x ∈ v
[PROOFSTEP]
exact mem_of_mem_nhds hv
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
[PROOFSTEP]
simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff,
  continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
[PROOFSTEP]
simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ (x : α), x ∈ s → LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
[PROOFSTEP]
exact ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
[PROOFSTEP]
simp_rw [continuous_iff_continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn, lowerSemicontinuousOn_univ_iff,
  upperSemicontinuousOn_univ_iff]


[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
⊢ HasCountableSeparatingOn X IsOpen s
[PROOFSTEP]
suffices HasCountableSeparatingOn s IsOpen univ from .of_subtype fun _ ↦ isOpen_induced_iff.1
[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
⊢ HasCountableSeparatingOn (↑s) IsOpen univ
[PROOFSTEP]
refine ⟨⟨countableBasis s, countable_countableBasis _, fun _ ↦ isOpen_of_mem_countableBasis, fun x _ y _ h ↦ ?_⟩⟩
[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
x : ↑s
x✝¹ : x ∈ univ
y : ↑s
x✝ : y ∈ univ
h : ∀ (s_1 : Set ↑s), s_1 ∈ countableBasis ↑s → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y
[PROOFSTEP]
exact ((isBasis_countableBasis _).inseparable_iff.2 h).eq