AntivaryOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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