strictMonoOn_of_lt_succ — Mathlib

English

Let s be Ord-connected. If for every a not maximal, with a ∈ s and succ a ∈ s we have f(a) < f(succ a), then f is strictly monotone on s.

Русский

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

LaTeX

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

Lean4

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

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