sub_fst — Mathlib

English

Let x, y be elements of the doubled module with components in E and F, i.e. x, y ∈ C⋆ᵐᵒᵈ(A, E × F). Then the first component of their difference is the difference of their first components: (x − y).fst = x.fst − y.fst.

Русский

Пусть x, y ∈ C⋆ᵐᵒᵈ(A, E × F). Тогда первая компонента разности равна разности первых компонент: (x − y).fst = x.fst − y.fst.

LaTeX

$$$$ (x - y).fst = x.fst - y.fst $$$$

Lean4

@[simp]
theorem sub_fst : (x - y).fst = x.fst - y.fst :=
  rfl

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