span_setOf_mem_eq_top — Mathlib

English

The span of the preimage of s under the inclusion map from span R s to M is the whole ambient space, i.e., equals ⊤.

Русский

Образ порождаемой области через включение inversely восстанавливает всю оболочку: span R (((↑) : span R s → M) )^{-1}(s) порождает ⊤.

LaTeX

$$$$\operatorname{span} R \big( (\uparrow)^{-1}(s) \big) = \top$$$$

Lean4

@[simp]
theorem span_setOf_mem_eq_top : span R {x : span R s | (x : M) ∈ s} = ⊤ :=
  span_span_coe_preimage

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