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

Composable

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)

  45structure Composable (M : CostModel A) where
  46  comp : A → A → A
  47  subadd : ∀ a b, M.cost (comp a b) ≤ M.cost a + M.cost b
  48  mono : ∀ a a' b b', Prefer M a a' → Prefer M b b' → Prefer M (comp a b) (comp a' b')
  49  strict_mono_left : ∀ a a' x, Improves M a a' → Improves M (comp a x) (comp a' x)
  50
  51/-- Monotonicity of composition w.r.t. preference. -/

used by (3)

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

depends on (20)

Lean names referenced from this declaration's body.