liftInclusion_of — Mathlib

English

The lift-inclusion evaluates to the natural subtype embedding on the i-th component.

Русский

Лифт-включение на i-ом компоненте совпадает с встроенным включением подструктуры.

LaTeX

$$$\mathrm{liftInclusion}\;S\bigl(\mathrm{of}_{L\,\iota\,G\,f,i}(x)\bigr) = \mathrm{Substructure.subtype}(S_i)\,x.$$$

Lean4

theorem liftInclusion_of {i : ι} (x : S i) :
    (liftInclusion S) (of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i x) =
      Substructure.subtype (S i) x :=
  rfl

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