ι : Type ?u.254167
ι' : Type ?u.254170
α : Type u_1
β : Type u_2
γ : Type ?u.254179
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → β
l : Filter β
⊢ (∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → b ∈ f ⁻¹' s) ↔ ∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → f b ∈ s
ι : Type ?u.254167
ι' : Type ?u.254170
α : Type u_1
β : Type u_2
γ : Type ?u.254179
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → β
l : Filter β
⊢ Tendsto f atTop l ↔ ∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → f b ∈ s
simp only [tendsto_def, mem_atTop_sets]
no goals
ι : Type ?u.254167
ι' : Type ?u.254170
α : Type u_1
β : Type u_2
γ : Type ?u.254179
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → β
l : Filter β
⊢ (∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → b ∈ f ⁻¹' s) ↔ ∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → f b ∈ s
rfl