fst — Mathlib

English

Supremum of two IsLittleOTVS relations equates to the pairwise IsLittleOTVS relation for the coordinate-wise product.

Русский

Супремум двух IsLittleOTVS равенство парной IsLittleOTVS для координатного произведения.

LaTeX

$$$\\text{IsLittleOTVS}(l, f, g) \\text{ и } \\text{IsLittleOTVS}(l, h, g) \\Rightarrow \\text{IsLittleOTVS}(l, (f, h), g).$$$

Lean4

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

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