English
For any f: α → β, a ∈ α, l a filter on α, the coinduced topology satisfies coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l).
Русский
Для отображения f: α → β, точки a и фильтра l на α справедливо равенство коиндуцированной топологии: coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l).
LaTeX
$$$\\mathrm{coinduced}\\ f\\ (\\mathrm{nhdsAdjoint}\\ a\\ l) = \\mathrm{nhdsAdjoint}\\ (f\\ a) (\\operatorname{map} f\\ l).$$$
Lean4
theorem coinduced_nhdsAdjoint (f : α → β) (a : α) (l : Filter α) :
coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l) :=
eq_of_forall_ge_iff fun _ ↦ by rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]
