strictMonoOn_of_pred_lt — Mathlib

English

Let s be Ord-connected. If for all a not minimal with a ∈ s and pred a ∈ s we have f(pred a) < f a, then StrictMonoOn f s.

Русский

Пусть s ордерно-соединено. Если для каждого a, не минимального, с a ∈ s и pred a ∈ s, выполняется f(pred a) < f(a), то StrictMonoOn f s.

LaTeX

$$$\\operatorname{OrdConnected}(s) \\to \\Big( \\forall a, \\neg \\operatorname{IsMin}(a) \\to a \\in s \\to \\operatorname{pred}(a) \\in s \\to f(\\operatorname{pred}(a)) < f(a) \\Big) \\to \\operatorname{StrictMonoOn}(f,s).$$$

Lean4

theorem strictMonoOn_of_pred_lt (hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a) :
    StrictMonoOn f s := by
  rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le
  obtain _ | n := n
  · simp at hab
  apply not_isMin_of_lt at hab
  induction n with
  | zero => simpa using hf _ hab hb ha
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n + 1] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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