injective_sum_to — Mathlib

English

The range of sum_to is exactly the union of GoodProducts π and MaxProducts.

Русский

Образ отображения sum_to равен объединению GoodProducts π и MaxProducts.

LaTeX

$$$\\operatorname{range}(\\mathrm{sum\\_to} C ho) = \\mathrm{GoodProducts}(\\pi C (ord I ·< o)) \\cup \\mathrm{MaxProducts} C ho$$$

Lean4

theorem injective_sum_to : Function.Injective (sum_to C ho) :=
  by
  refine
    Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
      (fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ (fun (hab : a = b) ↦ ?_))
  rw [← hab] at hb
  have ha' := Products.prop_of_isGood C _ ha (term I ho) hb.2
  simp only [ord_term_aux, lt_self_iff_false] at ha'

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