snd_sdiff

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#snd_sdiff

English

In α × β with SDiff defined componentwise, the second coordinate of a \ b equals a₂ \ b₂: (a \ b)₂ = a₂ \ b₂.

Русский

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

LaTeX

$$$ (a \ b)_2 = a_2 \ b_2 $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru