span_range_inclusionSpan — Mathlib

English

The span over S of the range of the inclusion map is the top submodule.

Русский

Покрытие Span над S диапазона включения даёт верхний подмодуль.

LaTeX

$$$\operatorname{span}_S(\operatorname{range}(\operatorname{inclusion} S p)) = \top$$$

Lean4

theorem span_range_inclusionSpan : span S (range <| p.inclusionSpan S) = ⊤ :=
  by
  have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by ext;
    simpa [Subtype.ext_iff] using fun h ↦ subset_span h
  apply map_injective_of_injective (span S (p : Set M)).injective_subtype
  rw [map_subtype_top, map_span, this]

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