lift'_closure — Mathlib

English

If f is continuous and f l l', then Tendsto f from l.lift' closure to l'.lift' closure.

Русский

Если f непрерывна и Tendsto f l l', то Tendsto f (l.lift' closure) (l'.lift' closure).

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow \\forall l\,l',\\ Tendsto\\ f\\ l\\ l' \\Rightarrow \\ Tendsto\\ f\\ (l.lift'\\text{ closure})\\ (l'.lift'\\text{ closure})$$$

Lean4

theorem lift'_closure (hf : Continuous f) {l l'} (h : Tendsto f l l') :
    Tendsto f (l.lift' closure) (l'.lift' closure) :=
  tendsto_lift'.2 fun s hs ↦ by filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

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