ltByCases_eq — Mathlib

English

If x = y, then ltByCases x y h1 h2 h3 equals h2 h, i.e., the equality branch is chosen when x=y.

Русский

Если x = y, то ltByCases x y h1 h2 h3 равно h2 h, то есть выбирается ветвь равенства, когда x = y.

LaTeX

$$$ ltByCases(x, y, h_1, h_2, h_3) = h_2(h) \\; (\\text{при } h: x = y) $$$

Lean4

@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltByCases_eq (h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} : ltByCases x y h₁ h₂ h₃ = h₂ h :=
  (dif_neg h.not_lt).trans (dif_neg h.not_gt)

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