sorted_divisorsAntidiagonalList_fst

English

The list n.divisorsAntidiagonalList is sorted by the first component in increasing order.

Русский

Список n.divisorsAntidiagonalList отсортирован по первой компоненте по возрастанию.

LaTeX

$$$\mathrm{DivisorsAntidiagonalList}(n)\ \text{Sorted by } (\cdot .\mathrm{fst})$$$

Lean4

theorem sorted_divisorsAntidiagonalList_fst {n : ℕ} : n.divisorsAntidiagonalList.Sorted (·.fst < ·.fst) :=
  by
  refine (List.sorted_lt_range' _ _ Nat.one_ne_zero).filterMap fun a b c d h h' ha => ?_
  rw [Option.ite_none_right_eq_some, Option.some.injEq] at h h'
  simpa [← h.right, ← h'.right]

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