stabilizerEquiv_invFun_eq — Mathlib

English

A canonical mapping evaluated at a fiber index i sends the corresponding inverse action to the fiber permutation at a chosen representative.

Русский

Каноническое отображение, применённое к индексу f(a)=i, присваивает соответствующее действие на волокне.

LaTeX

$$stabilizerEquiv_invFun g a = g i ⟨a, h⟩$$

Lean4

theorem stabilizerEquiv_invFun_eq (g : ∀ i, Perm { a // f a = i }) {a : α} {i : ι} (h : f a = i) :
    stabilizerEquiv_invFun g a = g i ⟨a, h⟩ := by subst h; rfl

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