fst — Mathlib

English

The first and second projection maps from a product space E × F are bounded linear maps.

Русский

Проекции fst и snd из произведения E × F являются ограниченными линейными отображениями.

LaTeX

$$$ \\text{fst} : E \\times F \\to E, \\; \\text{snd} : E \\times F \\to F; \\; \\|\\text{fst}\\|, \\|\\text{snd}\\| < \\infty $$$

Lean4

theorem fst : IsBoundedLinearMap 𝕜 fun x : E × F => x.1 :=
  by
  refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_
  rw [one_mul]
  exact le_max_left _ _

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