strictAntiOn_insert_iff_of_forall_ge

English

If ha states ∀ x ∈ s, a ≤ x, then StrictAntiOn f (insert a s) iff (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s.

Русский

Если ∀ x∈s, a ≤ x, то StrictAntiOn f (insert a s) эквивалентно (∀ b ∈ s, a < b → f b < f a) и StrictAntiOn f s.

LaTeX

$$$\forall x \in s, a \le x \Rightarrow \operatorname{StrictAntiOn}(f,\operatorname{insert}(a,s)) \iff \Big( \forall b \in s, a < b \to f(b) < f(a)\Big) \land \operatorname{StrictAntiOn}(f,s)$$$

Lean4

theorem strictAntiOn_insert_iff_of_forall_ge {a : α} (ha : ∀ x ∈ s, a ≤ x) :
    StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s :=
  by
  rw [strictAntiOn_insert_iff]
  have : ∀ b ∈ s, b < a → f a < f b := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
  tauto

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