comp_stabilizerEquiv_invFun — Mathlib

English

There is a multiplicative equivalence from the opposite of the stabilizer to a product of fiber permutations.

Русский

Существует мультипликативное эквивалентное отображение от противоположного стабилизатора к произведению перестановок по волокнам.

LaTeX

$$stabilizerMulEquiv : (stabilizer (Perm α)ᵈᵐᵃ f)ᵐᵒᵖ ≃* (∀ i, Perm { a // f a = i })$$

Lean4

theorem comp_stabilizerEquiv_invFun (g : ∀ i, Perm { a // f a = i }) (a : α) : f (stabilizerEquiv_invFun g a) = f a :=
  (g (f a) ⟨a, rfl⟩).prop

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