map_mapsTo_Iic_iff_tendsto — Mathlib

English

Let F and G be filters on α and β, and let m: α → β. Then the pushforward along m sends every subfilter of F into a subfilter of G if and only if m tends from F to G, i.e. Tendsto m F G.

Русский

Пусть F и G – фильтры на α и β, а m: α → β – функция. Тогда отображение по m отправляет каждый подфильтр F в подфильтр G тогда и только тогда, когда m сходится от F к G, т.е. Tendsto m F G.

LaTeX

$$$\mathrm{MapsTo}(\mathrm{map}\, m)\,(\mathrm{Iic}\, F)\,(\mathrm{Iic}\, G) \iff \mathrm{Tendsto}\, m\, F\, G$$

Lean4

theorem map_mapsTo_Iic_iff_tendsto {m : α → β} : MapsTo (map m) (Iic F) (Iic G) ↔ Tendsto m F G :=
  ⟨fun hm ↦ hm right_mem_Iic, fun hm _ ↦ hm.mono_left⟩

Похожие утверждения