GameAdd

Mathlib.Order.GameAdd

URI: https://scilib.ai/kg/mathlib#Sym2.GameAdd

Lean4

/-- `Sym2.GameAdd rα x y` means that `x` can be reached from `y` by decreasing either entry with
  respect to the relation `rα`.

  See `Prod.GameAdd` for the ordered pair analog. -/
def GameAdd (rα : α → α → Prop) : Sym2 α → Sym2 α → Prop :=
  Sym2.lift₂
    ⟨fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), fun a₁ b₁ a₂ b₂ =>
      by
      dsimp
      rw [Prod.gameAdd_swap_swap_mk _ _ b₁ b₂ a₁ a₂, Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂]
      simp [or_comm]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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