map_involutive — Mathlib

English

If f preserves p in a way that makes f an involution, then Subtype.map f h is also an involution.

Русский

Если f сохраняет p так, что он является инволютивным, то Subtype.map f h также является инволютивным.

LaTeX

$$$\\text{Involutive}(\\mathrm{Subtype}.map f h)$$$

Lean4

theorem map_involutive {p : α → Prop} {f : α → α} (h : ∀ a, p a → p (f a)) (hf : Involutive f) : Involutive (map f h) :=
  fun x ↦ Subtype.ext (hf x)

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