subtypePermOfFintype_one — Mathlib

English

If f is the identity on the whole α, the induced subtype permutation is the identity on the subtype.

Русский

Если f — тождественная на всём α, индуцированная перестановка на подтипе тоже тождественна.

LaTeX

$$$\\forall {f : \\mathrm{Perm}(\\alpha)} (h : ∀ x, p x → p ((1 : \\mathrm{Perm}(\\alpha)) x)), \\mathrm{subtypePermOfFintype}(1\, h) = 1$$$

Lean4

theorem subtypePermOfFintype_one (p : α → Prop) [Finite { x // p x }] (h : ∀ x, p x → p ((1 : Perm α) x)) :
    @subtypePermOfFintype α 1 p _ h = 1 :=
  rfl

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