def definition def or abbrev

`isMagic`

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

formal statement (Lean)

  36def isMagic (x : ℕ → ℝ) (Z : ℕ) : Prop :=

Definition body.

  37  ∃ s : ℕ, s ≤ Z ∧ isClosure x s
  38
  39end Octave
  40end Nuclear
  41end IndisputableMonolith
  42
  43
  44
  45
  46
  47
  48
  49

Lean names referenced from this declaration's body.