English
Let p be a predicate on α and f a permutation of α that preserves p in both directions, i.e. ∀x, p(f x) ↔ p x. Then the induced permutation on the subset {x ∈ α | p x} acts by x ↦ f x, with a witness showing p(f x).
Русский
Пусть p : α → ∖Prop и f — перестановка α такая, что p сохраняется при f: ∀x, p(f x) ↔ p x. Тогда на подмножестве {x ∈ α | p x} действует перестановка, полученная из f, и она отправляет x ↦ f x, причём существует свидетельство p(f x).
LaTeX
$$$$(\\mathrm{subtypePerm} f h)(\\langle a, ha \\rangle) = \\langle f(a), (h a).2\, ha \\rangle.$$$$
Lean4
@[simp]
theorem subtypePerm_apply (f : Perm α) (h : ∀ x, p (f x) ↔ p x) (x : { x // p x }) :
subtypePerm f h x = ⟨f x, (h _).2 x.2⟩ :=
rfl
