Monovary — Mathlib

English

MonovaryOn on s is equivalent to Monovary on the restricted domain s. In particular, restricting indices to s preserves the monovary relation.

Русский

MonovaryOn на s эквивалентна Monovary на ограниченной области s. В частности, ограничение индексов до s сохраняет отношение моновария.

LaTeX

$$$MonovaryOn(f,g,s) \iff Monovary(\lambda i:s. f i) (\lambda i:s. g i)$$$

Lean4

/-- `f` monovaries with `g` if `g i < g j` implies `f i ≤ f j`. -/
def Monovary (f : ι → α) (g : ι → β) : Prop :=
  ∀ ⦃i j⦄, g i < g j → f i ≤ f j

Похожие утверждения