swap — Mathlib

English

Swap symmetry for LiftRelAux: LiftRelAux (swap R) (swap C) b a equals LiftRelAux R C a b.

Русский

Обмен местами для LiftRelAux: LiftRelAux (swap R) (swap C) b a = LiftRelAux R C a b.

LaTeX

$$$\\mathrm{LiftRelAux}\\,(\\mathrm{swap}\\ R)\\,(\\mathrm{swap}\\ C)\\ b\\ a = \\mathrm{LiftRelAux}\\,R\\ C\\ a\\ b$$$

Lean4

theorem swap (R : α → β → Prop) (C) (a b) : LiftRelAux (swap R) (swap C) b a = LiftRelAux R C a b := by
  rcases a with a | ca <;> rcases b with b | cb <;> simp only [LiftRelAux]

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