IccExtendCM_of_mem — Mathlib

English

If x ∈ Icc a b, the extended map at x equals the original value at x; i.e., extension preserves the left endpoint values.

Русский

Если x ∈ Icc a b, то значение расширенного отображения в x равно исходному значению в x.

LaTeX

$$\\text{IccExtendCM}_ { | mem }: \\forall x \\in Icc(a,b), (IccExtendCM f) x = f x$$

Lean4

@[simp]
theorem IccExtendCM_of_mem {f : C(Icc a b, E)} {x : α} (hx : x ∈ Icc a b) : IccExtendCM f x = f ⟨x, hx⟩ := by
  simp [IccExtendCM, projIccCM, projIcc, hx.1, hx.2]

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