ramificationIdx_lt — Mathlib

English

If there exists no k with map f p ≤ P^k, then ramificationIdx f p P is less than n for any n.

Русский

Если не существует k с map f p ≤ P^k, то ramificationIdx f p P меньше любого n.

LaTeX

$$$\\text{If } hgt : ¬(map f p ≤ P^n) \\text{ then } ramificationIdx f p P < n$$$

Lean4

theorem ramificationIdx_lt {n : ℕ} (hgt : ¬map f p ≤ P ^ n) : ramificationIdx f p P < n := by
  classical
  rcases n with - | n
  · simp at hgt
  · rw [Nat.lt_succ_iff]
    have : ∀ k, map f p ≤ P ^ k → k ≤ n :=
      by
      refine fun k hk => le_of_not_gt fun hnk => ?_
      exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
    rw [ramificationIdx_eq_find ⟨n, this⟩]
    exact Nat.find_min' ⟨n, this⟩ this

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