pith. machine review for the scientific record. sign in
theorem proved term proof

gap_decreasing

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  58theorem gap_decreasing {N₁ N₂ : ℝ} (h₁ : 0 < N₁) (h_lt : N₁ < N₂) :
  59    gapToCapacity N₂ < gapToCapacity N₁ := by

proof body

Term-mode proof.

  60  unfold gapToCapacity
  61  have h₂ : 0 < N₂ := lt_trans h₁ h_lt
  62  have hp : 0 < phi := phi_pos
  63  have hphi_N1 : 0 < phi * N₁ := mul_pos hp h₁
  64  have hphi_N2 : 0 < phi * N₂ := mul_pos hp h₂
  65  -- 1 / (phi * N₂) < 1 / (phi * N₁) since phi * N₁ < phi * N₂
  66  have h_lt' : phi * N₁ < phi * N₂ := mul_lt_mul_of_pos_left h_lt hp
  67  exact one_div_lt_one_div_of_lt hphi_N1 h_lt'
  68
  69/-- Doubling N halves the gap. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.