go_fuel_irrel — Mathlib

English

From a count inequality, one derives the existence of an x meeting p within a boundary interval.

Русский

Из неравенства счёта выводится существование элемента x внутри интервала, удовлетворяющего p.

LaTeX

$$$\operatorname{count}(p,a) < \operatorname{count}(p,b) \Rightarrow \exists x \in \mathrm{Ico}(a,b),\ p(x)$$$

Lean4

theorem go_fuel_irrel (b : ℕ) (h : 2 ≤ b) (n fuel fuel' : ℕ) (hfuel : (if n = 0 then 0 else n + 1) < fuel)
    (hfuel' : (if n = 0 then 0 else n + 1) < fuel') : digitsAux.go b h n fuel hfuel = digitsAux.go b h n fuel' hfuel' :=
  by
  fun_induction go b h n fuel hfuel generalizing fuel'
  · rw [go_zero]
  · cases fuel'
    · simp at hfuel'
    · rw [go_succ]
      solve_by_elim

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