of_subtype_isSwap — Mathlib

English

If f : Perm (Subtype p) is a swap, then its image under ofSubtype is a swap.

Русский

Если f : Perm (Subtype p) — транспозиция, то (ofSubtype f) — транспозиция.

LaTeX

$$$$ \text{If } f:\operatorname{Perm}(\text{Subtype } p)\ \text{and } f\text{ IsSwap} \Rightarrow (\operatorname{ofSubtype} f) \text{ IsSwap}. $$$$

Lean4

theorem of_subtype_isSwap {p : α → Prop} [DecidablePred p] {f : Perm (Subtype p)} (h : f.IsSwap) :
    (ofSubtype f).IsSwap :=
  let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h
  ⟨x, y, by
    simp only [Ne, Subtype.ext_iff] at hxy
    exact hxy.1, by rw [hxy.2, ofSubtype_swap_eq]⟩

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