English
For WellFoundedLT I, the ℤ-span of the range of eval C equals the ℤ-span of the range of Products.eval C; hence the GoodProducts generate the same submodule as all products.
Русский
Пусть I хорошо упорядочено, тогда подмодуль, создаваемый целями eval C, совпадает с подмодулем, создаваемым Products.eval C.
LaTeX
$$$\\top \\;\\le\\; \\mathrm{Submodule}.\\mathrm{span}_{\\mathbb{Z}}(\\mathrm{range}(\\mathrm{eval}\\ C)) \\quad\\text{равно}\\quad \\top \\;\\le\\; \\mathrm{Submodule}.\\mathrm{span}_{\\mathbb{Z}}(\\mathrm{range}(\\mathrm{Products.eval}\\ C)).$$$
Lean4
/-- The good products span `LocallyConstant C ℤ` if and only all the products do. -/
theorem span_iff_products [WellFoundedLT I] :
⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C)) :=
by
refine ⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans h ?_⟩
rw [span_le]
rintro f ⟨l, rfl⟩
let L : Products I → Prop := fun m ↦ m.eval C ∈ span ℤ (Set.range (GoodProducts.eval C))
suffices L l by assumption
apply IsWellFounded.induction (· < · : Products I → Products I → Prop)
intro l h
dsimp
by_cases hl : l.isGood C
· apply subset_span
exact ⟨⟨l, hl⟩, rfl⟩
· simp only [Products.isGood, not_not] at hl
suffices Products.eval C '' {m | m < l} ⊆ span ℤ (Set.range (GoodProducts.eval C))
by
rw [← span_le] at this
exact this hl
rintro a ⟨m, hm, rfl⟩
exact h m hm
