fst_sdiff — Mathlib

English

In a product α × β where there is an SDiff operation defined coordinatewise, the first coordinate of a \ b equals a₁ \ b₁: (a \ b)₁ = a₁ \ b₁.

Русский

В произведении α × β, где операция SDiff определяется по координатам, первая координата a \ b равна a₁ \ b₁: (a \ b)₁ = a₁ \ b₁.

LaTeX

$$$ (a \ b)_1 = a_1 \ b_1 $$$

Lean4

@[simp]
theorem fst_sdiff [SDiff α] [SDiff β] (a b : α × β) : (a \ b).1 = a.1 \ b.1 :=
  rfl

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