prodExtendRight_apply_eq — Mathlib

English

The map prodExtendRight a e extends a permutation e ∈ Perm β to a permutation of Prod α × β by acting on the fiber over a and fixing other fibers.

Русский

Отображение prodExtendRight a e расширяет перестановку e ∈ Perm β на перестановку Prod α × β, действуя на волокне над a и фиксируя остальные волокна.

LaTeX

$$$prodExtendRight : Perm (\alpha_1 \times \beta_1) \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\n\text{toFun}(ab) = \text{if } ab.\mathrm{fst} = a \text{ then } (a, e(ab.snd)) \text{ else } ab$$$

Lean4

@[simp]
theorem prodExtendRight_apply_eq (b : β₁) : prodExtendRight a e (a, b) = (a, e b) :=
  if_pos rfl

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