small_span — Mathlib

English

If s is a small set of M, then span_R(s) is small.

Русский

Если s есть малый набор элементов M, тогда span_R(s) малый.

LaTeX

$$$Small(s) \Rightarrow Small(\operatorname{span}_R s)$$$

Lean4

theorem small_span [Small.{u} R] (s : Set M) [Small.{u} s] : Small.{u} (span R s) :=
  by
  suffices span R s = iSup (fun i : s ↦ span R ({(↑i : M)} : Set M))
    by
    rw [this]
    apply small_iSup
  simp [← Submodule.span_iUnion]

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