seq_decreasing — Mathlib

English

The sequence is strictly decreasing at all infinite places different from w1: if n < m, then for every w ≠ w1, w(algebra-map(seq m)) < w(algebra-map(seq n)).

Русский

Последовательность строго убывает на всех бесконечных местах, отличных от w1: если n < m, то для каждого w ≠ w1 выполняется w(алгебраическое отображение(seq m)) < w(алгебраическое отображение(seq n)).

LaTeX

$$$\forall n

Lean4

/-- The sequence is strictly decreasing at infinite places distinct from `w₁`. -/
theorem seq_decreasing {n m : ℕ} (h : n < m) (w : InfinitePlace K) (hw : w ≠ w₁) :
    w (algebraMap (𝓞 K) K (seq K w₁ hB m)) < w (algebraMap (𝓞 K) K (seq K w₁ hB n)) := by
  induction m with
  | zero =>
    exfalso
    exact Nat.not_succ_le_zero n h
  | succ m m_ih =>
    cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
    | inl hr =>
      rw [hr]
      exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
    | inr hr =>
      refine lt_trans ?_ (m_ih hr)
      exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

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