getD_min?_eq_untopD_minimum — Mathlib

English

For a linear-ordered α and a list l, l.min?.getD d equals l.minimum.untopD d.

Русский

Для линейного порядка α и списка l, l.min?.getD d равно l.minimum.untopD d.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)], \\forall l : \\List(\\alpha), \\forall d : \\alpha, \\bigl(l.min?.getD d = l.minimum.untopD d\\bigr)$$$

Lean4

theorem getD_min?_eq_untopD_minimum (l : List α) (d : α) : l.min?.getD d = l.minimum.untopD d :=
  getD_max?_eq_unbotD_maximum (α := αᵒᵈ) _ _

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