α : Type u_1
β : Type u_2
γ : Type ?u.347950
δ : Type ?u.347953
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
α : Type u_1
β : Type u_2
γ : Type ?u.347950
δ : Type ?u.347953
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
delta ContinuousWithinAt
α : Type u_1
β : Type u_2
γ : Type ?u.347950
δ : Type ?u.347953
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
α : Type u_1
β : Type u_2
γ : Type ?u.347950
δ : Type ?u.347953
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
  and_imp]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.347950
δ : Type ?u.347953
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
exact forall_congr' fun t => forall_swap