English
For any j, and WellFoundedLT, the extension d.Extension val₀ j is a Subsingleton; i.e., unique.
Русский
Для каждого j и WellFoundedLT extension d.Extension val₀ j образует Subsingleton; существует единственный элемент.
LaTeX
$$$\\text{Subsingleton}(d.\\mathrm{Extension}~val_0~j)$$$
Lean4
/-- An element in `d.Extension val₀ j` induces an element in `d.Extension val₀ i` when `i ≤ j`. -/
@[simps]
def ofLE {j : J} (e : d.Extension val₀ j) {i : J} (hij : i ≤ j) : d.Extension val₀ i
where
val := F.map (homOfLE hij).op e.val
map_zero := by
rw [← FunctorToTypes.map_comp_apply]
exact e.map_zero
map_succ k
hk := by
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, homOfLE_comp,
homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]
map_limit k hk
hki := by
rw [← FunctorToTypes.map_comp_apply, ← op_comp, homOfLE_comp, e.map_limit k hk (hki.trans hij)]
congr
ext ⟨l, hl⟩
dsimp
rw [← FunctorToTypes.map_comp_apply]
rfl
