strictMonoOn_insert_iff_of_forall_ge

English

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

Русский

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

LaTeX

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

Lean4

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

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