English
Let f be a monotone map from sets to sets (with respect to inclusion) and l a filter. Then membership of f(s) in l for all s ∈ 𝓝 x is equivalent to membership for all open s with x ∈ s.
Русский
Пусть f — монотонное отображение из множеств в множества и l — фильтр. Тогда члены множества f(s) принадлежат l для всех s ∈ 𝓝 x эквивалентны членству для всех открытых s с x ∈ s.
LaTeX
$$$\\forall s ∈ 𝓝 x,\ f(s) ∈ l \\quad\\iff\\quad \\forall s,\\ IsOpen(s) \\land x ∈ s \\Rightarrow f(s) ∈ l.$$$
Lean4
theorem all_mem_nhds_filter (x : X) (f : Set X → Set α) (hf : ∀ s t, s ⊆ t → f s ⊆ f t) (l : Filter α) :
(∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l :=
all_mem_nhds _ _ fun s t ssubt h => mem_of_superset h (hf s t ssubt)
