prodMk — Mathlib

English

The first and second projections are C^n maps and behave well under simp.

Русский

Первая и вторая проекции являются C^n отображениями и ведут себя гладко под simp.

LaTeX

$$$\text{fst}, \text{snd} \text{ are } C^n$; $\text{simp}$-lemmas drive simplifications.$$

Lean4

/-- Given two `C^n` maps `f` and `g`, this is the `C^n` map `x ↦ (f x, g x)`. -/
def prodMk (f : C^n⟮J, N; I, M⟯) (g : C^n⟮J, N; I', M'⟯) : C^n⟮J, N; I.prod I', M × M'⟯ :=
  ⟨fun x => (f x, g x), f.2.prodMk g.2⟩

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