def principal {α : Type u_1} (s : Set α) : Filter α

Equations

• principal s = { sets := {t : Set α | s ⊆ t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

def Tendsto₁ {X : Type u_1} {Y : Type u_2} (f : X → Y) (F : Filter X) (G : Filter Y) : Prop

Equations

• Tendsto₁ f F G = ∀ V ∈ G, f ⁻¹' V ∈ F

def Tendsto₂ {X : Type u_1} {Y : Type u_2} (f : X → Y) (F : Filter X) (G : Filter Y) : Prop

Equations

• Tendsto₂ f F G = (Filter.map f F ≤ G)