strictMonoOn_insert_iff_of_forall_le

English

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

Русский

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

LaTeX

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

Lean4

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

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