pith. machine review for the scientific record. sign in
lemma proved tactic proof

cast_lt_zero_iff

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)

  64lemma cast_lt_zero_iff {z : Int} : ((z : ℝ) < 0) ↔ z < 0 := by

proof body

Tactic-mode proof.

  65  constructor
  66  · intro hz
  67    by_contra h
  68    have : (0 : Int) ≤ z := le_of_not_gt h
  69    have : (0 : ℝ) ≤ (z : ℝ) := by exact_mod_cast this
  70    exact (not_lt_of_ge this) hz
  71  · intro hz
  72    exact_mod_cast hz
  73

used by (2)

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