English
If ha states that every x in s satisfies a ≤ x, then StrictAntiOn f (insert a s) iff (i) for all b ∈ s, a < b → f b < f a and (ii) StrictAntiOn f s.
Русский
Если для всех x∈s верно a ≤ x, то StrictAntiOn f (insert a s) эквивалентно (i) для всех b∈s, a < b → f b < f a и (ii) StrictAntiOn f s.
LaTeX
$$$\Big(\forall b \in s, a < b \to f b < f a\Big) \land \operatorname{StrictAntiOn}(f,s)$ включено в эквивалент, когда $\operatorname{StrictAntiOn}(f,\operatorname{insert}(a,s))$.$$
Lean4
theorem strictAntiOn_insert_iff {a : α} :
StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, b < a → f a < f b) ∧ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s :=
@strictMonoOn_insert_iff α βᵒᵈ _ _ _ _ _
