rel_perm — Mathlib

English

Forall₂ r ∘r Perm equals Perm ∘r Forall₂ r; i.e., applying a permutation and then Forall₂ r is equivalent to first Forall₂ r and then permuting.

Русский

Forall₂ r ∘r Perm равно Perm ∘r Forall₂ r; то есть применение перестановки, затем Forall₂ r эквивалентно сначала Forall₂ r, затем перестановке.

LaTeX

$$$\\mathrm{Forall}_2(r) \\circ_r \\mathrm{Perm} = \\mathrm{Perm} \\circ_r \\mathrm{Forall}_2(r)$$$

Lean4

theorem rel_perm (hr : BiUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· ↔ ·)) Perm Perm := fun _a _b hab _c _d hcd =>
  Iff.intro (rel_perm_imp hr.2 hab hcd) (rel_perm_imp hr.left.flip hab.flip hcd.flip)

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