map_mapsTo_Iic_iff_mapsTo — Mathlib

English

Let s ⊆ α, t ⊆ β, and m: α → β. The pushforward along m sends the down-set of the principal filters generated by s to that generated by t if and only if m maps s into t.

Русский

Пусть s ⊆ α, t ⊆ β, и m: α → β. Отображение по m переводит down-set (Iic) порождённого s в down-set Iic порождённого t тогда и только тогда, когда m картирует s в t.

LaTeX

$$$\mathrm{MapsTo}(\mathrm{map}\, m)\,(\mathrm{Iic}\lvert\mathcal{P}s\rangle)\,(\mathrm{Iic}\lvert\mathcal{P}t\rangle) \iff \mathrm{MapsTo}\, m\ s\ t$$

Lean4

theorem map_mapsTo_Iic_iff_mapsTo {s : Set α} {t : Set β} {m : α → β} :
    MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ MapsTo m s t := by
  rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]

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