ltByCases_gt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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