P3_comm

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.P3_comm

English

Let P3 be the relation on quadruples. Then P3(x1,x2,y1,y2) holds iff P3(y1,y2,x1,x2) holds.

Русский

Пусть P3 — отношение на кортежах; тогда P3(x1,x2,y1,y2) эквивалентно P3(y1,y2,x1,x2).

LaTeX

$$$$ \mathrm{P3}(x_1,x_2,y_1,y_2) \iff \mathrm{P3}(y_1,y_2,x_1,x_2). $$$$

Lean4

theorem P3_comm : P3 x₁ x₂ y₁ y₂ ↔ P3 y₁ y₂ x₁ x₂ :=
  by
  rw [P3, P3, add_comm]
  congr! 2 <;> rw [quot_mul_comm]

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

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

Разделы

Аффилиация

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