prod_apply — Mathlib

English

The product of two lines l and l' is a line in the sum type ι ⊕ ι' with idxFun given by Sum.elim l.idxFun l'.idxFun.

Русский

Произведение двух линий l и l' получается в линии над суммой индексов ι ⊕ ι' с индексной функцией Sum.elim l.idxFun l'.idxFun.

LaTeX

$$$\\forall l:\\ Line\\alpha\\ ι,\\ \\forall l':\\ Line\\alpha\\ ι',\\ \\forall x:\\alpha,\\ (l.prod\\ l')\\,x = \\mathrm{Sum.elim} (l\\,x) (l'\\,x).$$$

Lean4

@[simp]
theorem prod_apply {α ι ι'} (l : Line α ι) (l' : Line α ι') (x : α) : l.prod l' x = Sum.elim (l x) (l' x) :=
  by
  funext i
  cases i <;> rfl

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