MaxToGood — Mathlib

English

There is a canonical map sending each MaxProducts to a GoodProducts structure given by its Tail.

Русский

Существует естественный отображение, которое переводит MaxProducts в структуру GoodProducts через хвост.

LaTeX

$$$$\\mathrm{MaxToGood}\\; (h_1) :\\; \\mathrm{MaxProducts}\\; C\\; ho \\to \\mathrm{GoodProducts}\\; (C'\\,C\\;ho)$$$$

Lean4

/-- Given `l : MaxProducts C ho`, its `Tail` is a `GoodProducts (C' C ho)`. -/
noncomputable def MaxToGood (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (ord I · < o))))) :
    MaxProducts C ho → GoodProducts (C' C ho) := fun l ↦ ⟨l.val.Tail, maxTail_isGood C hC hsC ho l h₁⟩

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