strictMonoOn_insert_iff — Mathlib

English

StrictMonoOn on insert: StrictMonoOn f (insert a s) holds iff (i) for all b ∈ s, b < a → f b < f a and (ii) for all b ∈ s, a < b → f a < f b and (iii) StrictMonoOn f s.

Русский

Строго монотонность на вставке: StrictMonoOn f (insert a s) эквивалентна (i) для всех b∈s, b<a → f b < f a, (ii) для всех b∈s, a<b → f a < f b, и (iii) StrictMonoOn f s.

LaTeX

$$$\operatorname{StrictMonoOn}(f,\operatorname{insert}(a,s)) \iff \Big( \forall b\in s, b

Lean4

theorem strictMonoOn_insert_iff {a : α} :
    StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s := by
  simp [StrictMonoOn, forall_and]

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