localized'_span — Mathlib

English

Localization commutes with span: the localized' of span_R(s) equals span_S(f''(s)).

Русский

Локализация сохраняет операцию взятия порождающего множества: localized'(S,p,f)(span_R(s)) = span_S(f''(s)).

LaTeX

$$$\\operatorname{localized}'(S,p,f)(\\operatorname{span}_R(s)) = \\operatorname{span}_S\\big( f''(s) \\big).$$$

Lean4

@[simp]
theorem localized'_span (s : Set M) : (span R s).localized' S p f = span S (f '' s) := by
  rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]

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