English
The GoodProducts over C with respect to the successor o decompose as the union of GoodProducts over π and MaxProducts.
Русский
Добрые продукты над C по отношению к successor o распадаются на объединение GoodProducts над π и MaxProducts.
LaTeX
$$$\\mathrm{GoodProducts}(C) = \\mathrm{GoodProducts}(\\pi C (ord I ·< o)) \\cup \\mathrm{MaxProducts} C ho$$$
Lean4
theorem union_succ : GoodProducts C = GoodProducts (π C (ord I · < o)) ∪ MaxProducts C ho :=
by
ext l
simp only [GoodProducts, MaxProducts, Set.mem_union, Set.mem_setOf_eq]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· by_cases hh : term I ho ∈ l.val
· exact Or.inr ⟨h, hh⟩
· left
intro he
apply h
have h' := Products.prop_of_isGood_of_contained C _ h hsC
simp only [Order.lt_succ_iff] at h'
simp only at hh
have hh' : ∀ a ∈ l.val, ord I a < o := by
intro a ha
refine (h' a ha).lt_of_ne ?_
rw [ne_eq, ord_term ho a]
rintro rfl
contradiction
rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]
· refine h.elim (fun hh ↦ ?_) And.left
have := Products.isGood_mono C (Order.lt_succ o).le hh
rwa [contained_eq_proj C (Order.succ o) hsC]
