snd — Mathlib

English

A simp-variant of sup for LittleOTVS with a triple relation equality.

Русский

Упрощённый вариант sup для LittleOTVS с тройным равенством отношений.

LaTeX

$$$Eq(And(IsLittleOTVS(l,f,g), IsLittleOTVS(l,h,g)), IsLittleOTVS(l,(f,h),g)).$$$

Lean4

protected theorem snd {f : α → E × F} {g : α → G} (h : f =o[𝕜; l] g) : (f · |>.snd) =o[𝕜; l] g :=
  ContinuousLinearMap.snd 𝕜 E F |>.isBigOTVS_comp |>.trans_isLittleOTVS h

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