ltByCases_congr — Mathlib

English

For any x, y, and P, the equation ltByCases x y h1 h2 h3 = p holds if and only if p arises as the value of one of the branches (there exists a witness mapping to p from h1, h2, or h3).

Русский

Для любых x, y и P, равенство ltByCases x y h1 h2 h3 = p эквивалентно тому, что p равняется значению одной из ветвей (существует доказательство, переводящееся в p через h1, h2 или h3).

LaTeX

$$$ ltByCases(x, y, h_1, h_2, h_3) = p \\; \\iff \\; (\\exists h, h_1 h = p) \\lor (\\exists h, h_2 h = p) \\lor (\\exists h, h_3 h = p) $$$

Lean4

@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltByCases_congr {x' y' : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {h₁' : x' < y' → P}
    {h₂' : x' = y' → P} {h₃' : y' < x' → P} (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x'))
    (hh'₁ : ∀ (h : x' < y'), h₁ (ltc.mpr h) = h₁' h)
    (hh'₂ : ∀ (h : x' = y'), h₂ ((eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc).mpr h) = h₂' h)
    (hh'₃ : ∀ (h : y' < x'), h₃ (gtc.mpr h) = h₃' h) : ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃' :=
  by
  refine ltByCases_rec _ (fun h => ?_) (fun h => ?_) (fun h => ?_)
  · rw [ltByCases_lt (ltc.mp h), hh'₁]
  · rw [eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc] at h
    rw [ltByCases_eq h, hh'₂]
  · rw [ltByCases_gt (gtc.mp h), hh'₃]

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