zero_le_of_den — Mathlib

English

There exists an integer z with b = z for nth_partDen; i.e., every partDen corresponds to an integer.

Русский

Существует целое z такое, что b = z для nth_partDen; то есть каждое partDen соответствует целому числу.

LaTeX

$$$\\\\forall {K} {v} {n} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {b : K},\n (GenContFract.of v).partDens.get? n = Some b \\\\Rightarrow \\\\exists z : \\\\mathbb{Z}, b = (z : K)$$$

Lean4

/-- Shows that all denominators are nonnegative. -/
theorem zero_le_of_den : 0 ≤ (of v).dens n := by rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux];
  exact zero_le_of_contsAux_b

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