refl — Mathlib

English

The permutation obtained by applying subtypeCongr to identity on both sides is the identity permutation on the ambient type.

Русский

Перестановка, полученная оператором subtypeCongr от единичной перестановки по обеим подгруппам, является тождественной перестановкой на всей области.

LaTeX

$$$ \\text{Perm.subtypeCongr}(\\text{Equiv.refl }{ a \\mid p a }, \\text{Equiv.refl }{ a \\mid \\neg p a }) = \\text{Equiv.refl }\\varepsilon. $$$

Lean4

@[simp]
theorem refl : Perm.subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε :=
  by
  ext x
  by_cases h : p x <;> simp [h]

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