predAbove_right_monotone — Mathlib

English

For every n and every p ∈ Fin n, the map a ↦ p.predAbove a is monotone on Fin (n+1).

Русский

Для каждого n и каждого p ∈ Fin n, отображение a ↦ p.predAbove a монотонно на Fin(n+1).

LaTeX

$$$\forall {n : \mathbb{N}} (p : \mathrm{Fin}(n)), \; \text{Monotone}(p.predAbove)$$$

Lean4

theorem predAbove_right_monotone (p : Fin n) : Monotone p.predAbove := fun a b H =>
  by
  dsimp [predAbove]
  split_ifs with ha hb hb
  all_goals simp only [le_iff_val_le_val, coe_pred]
  · exact pred_le_pred H
  ·
    calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H
  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
  · exact H

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