mem_closure — Mathlib

English

If f is continuous within s at x and x is a limit point of s, and f maps s into t, then f x lies in closure of t.

Русский

Если f непрерывна внутри s в x и x является предельной точкой s, и f(s) ⊆ t, то f(x) ∈ closure(t).

LaTeX

$$$\text{ContinuousWithinAt } f\ s\ x \to x \in \overline{s} \to \text{MapsTo } f\ s\ t \to f(x) \in \overline{t}$$$

Lean4

theorem mem_closure {t : Set β} (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (ht : MapsTo f s t) :
    f x ∈ closure t :=
  closure_mono (image_subset_iff.2 ht) (h.mem_closure_image hx)

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