α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ RTendsto' r l (𝓝 a) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → Rel.preimage r s ∈ l
rw [rtendsto'_def]
case hf
α : Type u_2
β : Type u_1
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ ∀ (s t : Set α), s ⊆ t → Rel.preimage r s ⊆ Rel.preimage r t
α : Type u_2
β : Type u_1
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
apply all_mem_nhds_filter
no goals
case hf
α : Type u_2
β : Type u_1
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ ∀ (s t : Set α), s ⊆ t → Rel.preimage r s ⊆ Rel.preimage r t
apply Rel.preimage_mono