maxToGood_injective — Mathlib

English

The tail map that sends MaxProducts to GoodProducts is injective.

Русский

Отображение хвоста, переходящее из MaxProducts в GoodProducts, инъективно.

LaTeX

$$$$\\mathrm{Injective}\\; (\\mathrm{MaxToGood}\\; C\\; hC\\; hsC\\; ho\\; h_1)$$$$

Lean4

theorem maxToGood_injective (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (ord I · < o))))) :
    (MaxToGood C hC hsC ho h₁).Injective := by
  intro m n h
  apply Subtype.ext ∘ Subtype.ext
  rw [Subtype.ext_iff] at h
  dsimp [MaxToGood] at h
  rw [max_eq_o_cons_tail C hsC ho m, max_eq_o_cons_tail C hsC ho n, h]

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