subtypeCongr — Mathlib

English

Given permutations ep on {a|p a} and en on {a|¬p a}, one can construct a permutation on ε by acting as ep inside p and as en outside.

Русский

Для перестановок ep на {a|p a} и en на {a|¬p a} можно построить перестановку на ε, действуя внутри p и вне его.

LaTeX

$$$ \\text{Equiv.Perm.subtypeCongr }(ep,en) : \\text{Perm }\\varepsilon. $$$

Lean4

/-- Combining permutations on `ε` that permute only inside or outside the subtype
split induced by `p : ε → Prop` constructs a permutation on `ε`. -/
def subtypeCongr : Equiv.Perm ε :=
  permCongr (sumCompl p) (sumCongr ep en)

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