shrinkable — Mathlib

English

The rationals are shrinkable: the shrink operation on a rational r = a/b produces rationals with smaller numerators and denominators, enumerating simpler approximations.

Русский

Рациональные числа сжимаются: отображение сжатия числа r = a/b порождает рациональные числа с меньшими числителями и знаменателями, перечисляя более простые приближения.

LaTeX

$$$\text{shrink}(r)= (\text{Shrinkable.shrink}(r.num)).flatMap(\lambda d. (\text{Nat.shrink}(r.den)).map(\lambda n. \text{Rat.divInt}(d,n)))$$$

Lean4

instance shrinkable : Shrinkable Rat where
  shrink r := (Shrinkable.shrink r.num).flatMap fun d => Nat.shrink r.den |>.map fun n => Rat.divInt d n

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