flip — Mathlib

English

Forall₂ (flip R) b a implies Forall₂ R a b; i.e., reversing the pair order preserves the Forall₂ structure.

Русский

Forall₂ (flip R) b a следует из Forall₂ R a b; то есть смена порядка пары сохраняет структуру Forall₂.

LaTeX

$$$$ \\forall \\{a,b\\},\\ \\text{Forall₂} (\\mathrm{flip}\\ R)\\ b\\ a \\to \\text{Forall₂ } R\\ a\\ b. $$$$

Lean4

theorem flip : ∀ {a b}, Forall₂ (flip R) b a → Forall₂ R a b
  | _, _, Forall₂.nil => Forall₂.nil
  | _ :: _, _ :: _, Forall₂.cons h₁ h₂ => Forall₂.cons h₁ h₂.flip

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