English
If two successive differences are small, then the difference between the outermost polynomials is also small.
Русский
Если два последовательных различий малы, то и внешняя разность малы.
LaTeX
$$$cardPowDegree(x-y) < a \text{ and } cardPowDegree(y-z) < a \Rightarrow cardPowDegree(x-z) < a$$$
Lean4
/-- If `x` is close to `y` and `y` is close to `z`, then `x` and `z` are at least as close. -/
theorem cardPowDegree_anti_archimedean {x y z : Fq[X]} {a : ℤ} (hxy : cardPowDegree (x - y) < a)
(hyz : cardPowDegree (y - z) < a) : cardPowDegree (x - z) < a :=
by
have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
by_cases hxy' : x = y
· rwa [hxy']
by_cases hyz' : y = z
· rwa [← hyz']
by_cases hxz' : x = z
· rwa [hxz', sub_self, map_zero]
rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'
refine lt_of_le_of_lt ?_ (max_lt hxy hyz)
rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy', cardPowDegree_nonzero _ hyz']
have : (1 : ℤ) ≤ Fintype.card Fq := mod_cast (@Fintype.one_lt_card Fq _ _).le
simp only [le_max_iff]
refine Or.imp (pow_le_pow_right₀ this) (pow_le_pow_right₀ this) ?_
rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ← degree_eq_natDegree hxy', ←
degree_eq_natDegree hyz']
convert degree_add_le (x - y) (y - z) using 2
exact (sub_add_sub_cancel _ _ _).symm
