max_def — Mathlib

English

For x,y ∈ β*, the maximum in Germ β equals the germ of the maximum of the representatives: max x y = map₂ max x y.

Русский

Для гермов x,y ∈ β* максимум в Germ β равен герму максимума соответствующих представителей: max x y = map₂ max x y.

LaTeX

$$$\\max x y = \\mathrm{map}_2(\\max)\\, x\\, y.$$$

Lean4

theorem max_def [LinearOrder β] (x y : β*) : max x y = map₂ max x y :=
  inductionOn₂ x y fun a b => by
    rcases le_total (a : β*) b with h | h
    · rw [max_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_right hi).symm
    · rw [max_eq_left h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_left hi).symm

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