ι : Type ?u.256503
ι' : Type ?u.256506
α : Type u_2
β : Type u_1
γ : Type ?u.256515
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
s : Set α
⊢ (∃ a, ∀ (b : β), b ≥ a → b ∈ f ⁻¹' s) ↔ ∃ N, ∀ (n : β), n ≥ N → f n ∈ s
ι : Type ?u.256503
ι' : Type ?u.256506
α : Type u_2
β : Type u_1
γ : Type ?u.256515
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
s : Set α
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ (n : β), n ≥ N → f n ∈ s
rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets]
no goals
ι : Type ?u.256503
ι' : Type ?u.256506
α : Type u_2
β : Type u_1
γ : Type ?u.256515
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
s : Set α
⊢ (∃ a, ∀ (b : β), b ≥ a → b ∈ f ⁻¹' s) ↔ ∃ N, ∀ (n : β), n ≥ N → f n ∈ s
rfl