English
If x ≠ 0, y ≠ 0 and x+y ≠ 0, then the least well-founded element among the supports of x and y is ≤ the least well-founded element of the support of x+y.
Русский
Если x ≠ 0, y ≠ 0 и x+y ≠ 0, то наименьший элемент поддержки x и y по отношению к обычному порядку не превосходит наименьшего элемента поддержки x+y.
LaTeX
$$$$ \min\left( \operatorname{Set.IsWF.min} \big(x.isWF\_support\big), \operatorname{Set.IsWF.min} \big(y.isWF\_support\big) \right) \le \operatorname{Set.IsWF.min}\big((x+y).isWF\_support\big). $$$$
Lean4
protected theorem min_le_min_add {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0)
(hxy : x + y ≠ 0) :
min (Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx))
(Set.IsWF.min y.isWF_support (support_nonempty_iff.2 hy)) ≤
Set.IsWF.min (x + y).isWF_support (support_nonempty_iff.2 hxy) :=
by
rw [← Set.IsWF.min_union]
exact Set.IsWF.min_le_min_of_subset (support_add_subset (x := x) (y := y))
