mapsTo_span — Mathlib

English

If f maps s into N, then f maps span(s) into N.

Русский

Если отображение f отправляет каждое s в N, то оно отправляет span(s) в N.

LaTeX

$$$\text{MapsTo} (f)\, s\, t \Rightarrow \text{MapsTo}(f)\, \operatorname{span}(s) \operatorname{span} (t)$$$

Lean4

theorem mapsTo_span {f : F} {s : Set M} {t : Set M₂} (h : MapsTo f s t) : MapsTo f (span R s) (span R₂ t) :=
  (span_mono h).trans (span_preimage_le (σ₁₂ := σ₁₂) f t)

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