span — Mathlib

English

The good products span all LocallyConstant ℤ-valued functions on C when C is closed.

Русский

Если C замкнуто, хорошие произведения порождают всю модуль-структуру LocallyConstant C ℤ.

LaTeX

$$$ \top \le \operatorname{span}_{\mathbb{Z}} (\operatorname{Set.range}(\mathrm{eval}\ C)) $$$

Lean4

/-- The good products span all of `LocallyConstant C ℤ` if `C` is closed. -/
theorem span [WellFoundedLT I] (hC : IsClosed C) : ⊤ ≤ Submodule.span ℤ (Set.range (eval C)) :=
  by
  rw [span_iff_products]
  intro f _
  obtain ⟨K, f', rfl⟩ : ∃ K f', f = πJ C K f' := fin_comap_jointlySurjective C hC f
  refine
    Submodule.span_mono ?_ <|
      Submodule.apply_mem_span_image_of_mem_span (πJ C K) <| spanFin C K (Submodule.mem_top : f' ∈ ⊤)
  rintro l ⟨y, ⟨m, rfl⟩, rfl⟩
  exact ⟨m.val, eval_eq_πJ C K m.val m.prop⟩

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