tendsto' — Mathlib

English

For any t, Continuous f implies f^{-1}(Int t) ⊆ Int(f^{-1} t).

Русский

Для любого t, непрерывная f подразумевает f^{-1}(Int t) ⊆ Int(f^{-1} t).

LaTeX

$$$\\mathrm{Continuous}(f) \\Rightarrow f^{-1}(\\operatorname{Int}(t)) \\subseteq \\operatorname{Int}(f^{-1}(t))$$$

Lean4

/-- A version of `Continuous.tendsto` that allows one to specify a simpler form of the limit.
E.g., one can write `continuous_exp.tendsto' 0 1 exp_zero`. -/
theorem tendsto' (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Tendsto f (𝓝 x) (𝓝 y) :=
  h ▸ hf.tendsto x

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