predAbove_left_monotone — Mathlib

English

For every i ∈ Fin(n+1), the map p ↦ p.predAbove i is monotone in p.

Русский

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

LaTeX

$$$\forall {i : \mathrm{Fin}(n+1)}, \; \text{Monotone}(\lambda p : \mathrm{Fin}(n+1) \mapsto p.predAbove i)$$$

Lean4

theorem predAbove_left_monotone (i : Fin (n + 1)) : Monotone fun p ↦ predAbove p i := fun a b H ↦
  by
  dsimp [predAbove]
  split_ifs with ha hb hb
  · rfl
  · exact pred_le _
  · have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
    exact absurd H this.not_ge
  · rfl

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