pith. machine review for the scientific record. sign in
def definition def or abbrev

logIntervalMono

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)

  37def logIntervalMono (I : Interval) (_hI_pos : 0 < I.lo)
  38    (lo_bound hi_bound : ℚ)
  39    (_h_lo : (lo_bound : ℝ) ≤ log I.lo)
  40    (_h_hi : log I.hi ≤ (hi_bound : ℝ))
  41    (h_valid : lo_bound ≤ hi_bound) : Interval where
  42  lo := lo_bound

proof body

Definition body.

  43  hi := hi_bound
  44  valid := h_valid
  45

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.