projIcc_eq_right — Mathlib

English

projIcc(a,b,h,x) equals the right endpoint iff b ≤ x (with a < b).

Русский

projIcc(a,b,h,x) равно правому концу тогда и только тогда, когда b ≤ x (при a < b).

LaTeX

$$projIcc_eq_right(h,x) : projIcc(a,b,h,x) = ⟨b, right_mem_Icc.2 h⟩ ↔ b ≤ x$$

Lean4

theorem projIcc_eq_right (h : a < b) : projIcc a b h.le x = ⟨b, right_mem_Icc.2 h.le⟩ ↔ b ≤ x := by
  simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_ge]

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