restrictionLE_obj — Mathlib

English

The restriction of F to the segment below i evaluates at k as F.obj(k) for k < i with hi ≤ j.

Русский

Ограничение F до сегмента ниже i оценивается как F.obj(k) для k< i при hi.

LaTeX

$$restrictionLT_obj (k) (hk) : (restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.le.trans hi⟩$$

Lean4

@[simp]
theorem restrictionLE_obj (k : J) (hk : k ≤ i) : (restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.trans hi⟩ :=
  rfl

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