[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have ha : a ∈ Ici a := left_mem_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, b < f b_1
[PROOFSTEP]
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using
  hb.trans_le ((h_mono.le_iff_le has hxs).2 hxa)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rw [h_mono.lt_iff_lt has hcs] at hac 
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
filter_upwards [hs, Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 hac)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ (a_1 : α), a_1 ∈ s → a_1 ∈ Ico a c → f a_1 < b
[PROOFSTEP]
rintro x hx ⟨_, hxc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
[PROOFSTEP]
exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have ha : a ∈ Ici a := left_mem_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, b < f b_1
[PROOFSTEP]
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le (h_mono has hxs hxa)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
have : a < c := not_le.1 fun h => hac.not_le <| h_mono hcs has h
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
filter_upwards [hs, Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 this)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ (a_1 : α), a_1 ∈ s → a_1 ∈ Ico a c → f a_1 < b
[PROOFSTEP]
rintro x hx ⟨_, hxc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
[PROOFSTEP]
exact (h_mono hx hcs hxc.le).trans_lt hcb
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases(mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases exists_between hab' with ⟨c', hc'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with ⟨_, hc, ⟨c, hcs, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure (f '' univ) ∈ 𝓝 (f a)
[PROOFSTEP]
simp only [image_univ, h_dense.closure_eq, univ_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous ↑e
[PROOFSTEP]
rw [‹OrderTopology β›.topology_eq_generate_intervals]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous ↑e
[PROOFSTEP]
refine' continuous_generateFrom fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
s : Set β
hs : s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
⊢ IsOpen (↑e ⁻¹' s)
[PROOFSTEP]
rcases hs with ⟨a, rfl | rfl⟩
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (↑e ⁻¹' Ioi a)
[PROOFSTEP]
rw [e.preimage_Ioi]
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Ioi (↑(symm e) a))
[PROOFSTEP]
apply isOpen_lt'
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (↑e ⁻¹' Iio a)
[PROOFSTEP]
rw [e.preimage_Iio]
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Iio (↑(symm e) a))
[PROOFSTEP]
apply isOpen_gt'
