IccExtend_of_le_left — Mathlib

English

If x ≤ a, the left endpoint determines the value of the extended function on the interval Icc.

Русский

Если x ≤ a, значение расширения по левому концу задаётся через a.

LaTeX

$$$(\\mathrm{IccExtend} h f)(x) = f(a) \\quad\\text{если } x \\le a$$$

Lean4

theorem IccExtend_of_le_left (f : Icc a b → β) (hx : x ≤ a) : IccExtend h f x = f ⟨a, left_mem_Icc.2 h⟩ :=
  congr_arg f <| projIcc_of_le_left h hx

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