English
Let f : X ⇢ Y. Then PContinuous f is equivalent to: for all x, y with y ∈ f(x), PTendsto' f (nhds x) (nhds y).
Русский
Пусть f : X ⇢ Y. Тогда PContinuous f эквивалентно: для любых x и y, если y ∈ f(x), то PTendsto' f (nhds x) (nhds y).
LaTeX
$$$\\mathrm{PContinuous}(f) \\iff \\forall \\{x\\ and\\ }\\{y\\}, y \\in f(x) \\rightarrow \\mathrm{PTendsto'}\\,f\\,(\\mathcal{N}(x))\\,(\\mathcal{N}(y))$$$
Lean4
theorem pcontinuous_iff' {f : X →. Y} : PContinuous f ↔ ∀ {x y} (_ : y ∈ f x), PTendsto' f (𝓝 x) (𝓝 y) :=
by
constructor
· intro h x y h'
simp only [ptendsto'_def, mem_nhds_iff]
rintro s ⟨t, tsubs, opent, yt⟩
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
intro hf s os
rw [isOpen_iff_nhds]
rintro x ⟨y, ys, fxy⟩ t
rw [mem_principal]
intro (h : f.preimage s ⊆ t)
apply mem_of_superset _ h
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
change f.preimage s ∈ 𝓝 x
apply h'
rw [mem_nhds_iff]
exact ⟨s, Set.Subset.refl _, os, ys⟩
