English
Characterization of antitone-on-insert: AntitoneOn f (insert a s) holds iff (i) for all b ∈ s, b ≤ a → f a ≤ f b; (ii) for all b ∈ s, a ≤ b → f b ≤ f a; and (iii) AntitoneOn f s.
Русский
Характеризация антитоничности на вставке: AntitoneOn f (insert a s) эквивалентна (i) для всех b∈s: b ≤ a ⇒ f(a) ≤ f(b); (ii) для всех b∈s: a ≤ b ⇒ f(b) ≤ f(a); (iii) AntitoneOn f s.
LaTeX
$$$\operatorname{AntitoneOn}(f,\operatorname{insert}(a,s)) \iff \Big( \forall b\in s, b\le a \to f(a) \le f(b)\Big) \\ \land\Big( \forall b\in s, a\le b \to f(b) \le f(a)\Big) \land \operatorname{AntitoneOn}(f,s)$$$
Lean4
theorem antitoneOn_insert_iff {a : α} :
AntitoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f a ≤ f b) ∧ (∀ b ∈ s, a ≤ b → f b ≤ f a) ∧ AntitoneOn f s :=
@monotoneOn_insert_iff α βᵒᵈ _ _ _ _ _
