strictAntiOn_insert_iff_of_forall_le

English

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

Русский

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

LaTeX

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

Lean4

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

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