perm_inv_on_of_perm_on_finite — Mathlib

English

Given a permutation f of α that preserves a predicate p with a finite set of its witnesses, one obtains a permutation on the subtype {x | p x} induced by f.

Русский

Дано перестановка f на α, сохраняющая предикат p; если множество {x | p x} конечно, то существует перестановка на подтипе {x | p x}, индукцированная f.

LaTeX

$$$\\text{abbrev }\\mathrm{subtypePermOfFintype}(f) : \\mathrm{Perm}(\\{x : \\alpha \\mid p x\\})$$$

Lean4

theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x)) {x : α}
    (hx : p x) : p (f⁻¹ x) := by
  have : Finite {x | p x} := by simpa
  simpa using perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx

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