case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f → ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ (∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
constructor
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)
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ (∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
intro hf s os
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)
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)
rw [isOpen_iff_nhds]
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
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)
rintro x ⟨y, ys, fxy⟩ t
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
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
rw [mem_principal]
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
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
intro (h : f.preimage s ⊆ t)
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
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
change t ∈ 𝓝 x
α : 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
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
apply mem_of_superset _ h
α : 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
α : 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
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
α : 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
α : 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
show f.preimage s ∈ 𝓝 x
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
α : 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
apply h'
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
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
rw [mem_nhds_iff]
no goals
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
exact ⟨s, Set.Subset.refl _, os, ys⟩
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)
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f → ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
intro h x y h'
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
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)
simp only [ptendsto'_def, mem_nhds_iff]
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
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
rintro s ⟨t, tsubs, opent, yt⟩
no goals
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
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
α : 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
α : 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
intro s hs
α : 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
α : 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
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
α : 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
α : 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
rw [ptendsto'_def] at this
no goals
α : 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
exact this s hs