getD_max?_eq_unbotD_maximum — Mathlib

English

For any list l in a linear order α and any d ∈ α, l.max?.getD d equals l.maximum.unbotD d.

Русский

Для списка l над линейным порядком α и любого элемента d ∈ α, выражение l.max?.getD d равно l.maximum.unbotD d.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)], \\forall l : \\mathrm List(\\alpha), \\forall d : \\alpha, \\bigl(l.max?.getD d = l.maximum.unbotD d\\bigr)$$$

Lean4

theorem getD_max?_eq_unbotD_maximum (l : List α) (d : α) : l.max?.getD d = l.maximum.unbotD d := by
  cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff_legacy] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)
      all_goals simp [le_total]

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