English
Characterization of monotone-on-insert: MonotoneOn f (insert a s) holds iff three conditions hold: (i) for all b in s with b ≤ a, f b ≤ f a; (ii) for all b in s with a ≤ b, f a ≤ f b; and (iii) MonotoneOn f s.
Русский
Характеризация монотонности на вставке: MonotoneOn f (insert a s) равносильна трём условиям: (i) для всех b ∈ s, b ≤ a ⇒ f(b) ≤ f(a); (ii) для всех b ∈ s, a ≤ b ⇒ f(a) ≤ f(b); (iii) MonotoneOn f s.
LaTeX
$$$\operatorname{MonotoneOn}(f,\operatorname{insert}(a,s)) \iff \Big( \forall b\in s, b\le a \to f(b) \le f(a)\Big) \\ \land\Big( \forall b\in s, a\le b \to f(a) \le f(b)\Big) \land \operatorname{MonotoneOn}(f,s)$$$
Lean4
theorem monotoneOn_insert_iff {a : α} :
MonotoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s := by
simp [MonotoneOn, forall_and]
