min_def — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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