[GOAL]
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ RTendsto' r l (𝓝 a) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → Rel.preimage r s ∈ l
[PROOFSTEP]
rw [rtendsto'_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ (∀ (s : Set α), s ∈ 𝓝 a → Rel.preimage r s ∈ l) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → Rel.preimage r s ∈ l
[PROOFSTEP]
apply all_mem_nhds_filter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ ∀ (s t : Set α), s ⊆ t → Rel.preimage r s ⊆ Rel.preimage r t
[PROOFSTEP]
apply Rel.preimage_mono
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.Dom f)
[PROOFSTEP]
rw [← PFun.preimage_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.preimage f Set.univ)
[PROOFSTEP]
exact h _ isOpen_univ
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f → ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
intro h x y h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
⊢ PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
simp only [ptendsto'_def, mem_nhds_iff]
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
⊢ ∀ (s : Set β), (∃ t, t ⊆ s ∧ IsOpen t ∧ y ∈ t) → ∃ t, t ⊆ PFun.preimage f s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro s ⟨t, tsubs, opent, yt⟩
[GOAL]
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
s t : Set β
tsubs : t ⊆ s
opent : IsOpen t
yt : y ∈ t
⊢ ∃ t, t ⊆ PFun.preimage f s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ (∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
[PROOFSTEP]
intro hf s os
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
⊢ IsOpen (PFun.preimage f s)
[PROOFSTEP]
rw [isOpen_iff_nhds]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
⊢ ∀ (a : α), a ∈ PFun.preimage f s → 𝓝 a ≤ 𝓟 (PFun.preimage f s)
[PROOFSTEP]
rintro x ⟨y, ys, fxy⟩ t
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
⊢ t ∈ 𝓟 (PFun.preimage f s) → t ∈ 𝓝 x
[PROOFSTEP]
rw [mem_principal]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
⊢ PFun.preimage f s ⊆ t → t ∈ 𝓝 x
[PROOFSTEP]
intro (h : f.preimage s ⊆ t)
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ t ∈ 𝓝 x
[PROOFSTEP]
change t ∈ 𝓝 x
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ t ∈ 𝓝 x
[PROOFSTEP]
apply mem_of_superset _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
  intro s hs
  have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
  rw [ptendsto'_def] at this 
  exact this s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
rw [ptendsto'_def] at this 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
this : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
exact this s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
show f.preimage s ∈ 𝓝 x
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
apply h'
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ s ∈ 𝓝 y
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ ∃ t, t ⊆ s ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
exact ⟨s, Set.Subset.refl _, os, ys⟩
