sum_to_range — Mathlib

English

There is an equivalence between the sum of GoodProducts and GoodProducts over C.

Русский

Существует эквиваленция между суммой GoodProducts и GoodProducts над C.

LaTeX

$$$\\mathrm{sum\\_equiv}: (\\mathrm{GoodProducts}(\\pi C (ord I · < o)) \\,⊕\, \\mathrm{MaxProducts} C ho) \\simeq \\mathrm{GoodProducts}(C)$$$

Lean4

theorem sum_to_range : Set.range (sum_to C ho) = GoodProducts (π C (ord I · < o)) ∪ MaxProducts C ho :=
  by
  have h : Set.range (sum_to C ho) = _ ∪ _ := Set.Sum.elim_range _ _; rw [h]; congr <;> ext l
  · exact ⟨fun ⟨m, hm⟩ ↦ by rw [← hm]; exact m.prop, fun hl ↦ ⟨⟨l, hl⟩, rfl⟩⟩
  · exact ⟨fun ⟨m, hm⟩ ↦ by rw [← hm]; exact m.prop, fun hl ↦ ⟨⟨l, hl⟩, rfl⟩⟩

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