map_nhdsWithin_eq — Mathlib

English

If e.IsImage s t and x ∈ e.source, then map e (nhdsWithin x s) = nhdsWithin (e x) t.

Русский

Если IsImage(e, s, t) и x ∈ e.source, то отображение e сохраняет nhdsWithin: map e (nhdsWithin x s) = nhdsWithin (e x) t.

LaTeX

$$IsImage(e, s, t) \\land x \\in e.source \\Rightarrow map(e, nhdsWithin x s) = nhdsWithin (e x) t$$

Lean4

theorem map_nhdsWithin_eq (h : e.IsImage s t) (hx : x ∈ e.source) : map e (𝓝[s] x) = 𝓝[t] e x := by
  rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]

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