MonovaryOn — Mathlib

English

If s ⊆ t and MonovaryOn f g t holds, then MonovaryOn f g s holds as well.

Русский

Если s ⊆ t и MonovaryOn f g t выполняется, то MonovaryOn f g s тоже выполняется.

LaTeX

$$$s \subseteq t \rightarrow MonovaryOn(f,g,t) \rightarrow MonovaryOn(f,g,s)$$$

Lean4

/-- `f` monovaries with `g` on `s` if `g i < g j` implies `f i ≤ f j` for all `i, j ∈ s`. -/
def MonovaryOn (f : ι → α) (g : ι → β) (s : Set ι) : Prop :=
  ∀ ⦃i⦄ (_ : i ∈ s) ⦃j⦄ (_ : j ∈ s), g i < g j → f i ≤ f j

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