monotoneOn_of_le_succ — Mathlib

English

Let s be an Ord-connected subset of α. If for every a not maximal, whenever a ∈ s and succ a ∈ s, we have f(a) ≤ f(succ(a)), then f is monotone on s.

Русский

Пусть s ⊆ α — множества, удовлетворяющее свойству орд-соединённости. Если для каждого 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) \\le f(\\operatorname{succ}(a))) \\Big) \\to \\operatorname{MonotoneOn}(f,s).$$$

Lean4

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

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