sameCycle_subtypePerm — Mathlib

English

Extending the domain via a bijection f interacts with the cycle structure: SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y.

Русский

Расширение области определения через биекция f взаимодействует со структурой циклов: SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y.

LaTeX

$$$\\forall p:\\beta\\to\\mathrm{Prop} \\;[\\mathrm{DecidablePred}\,p],\\; f:\\alpha\\xrightarrow{\\cong} \\text{Subtype}(p),\\; g:\\alpha\\to\\alpha,\\; (g\\extendDomain f).SameCycle (f x).val (f y).val \\iff g.SameCycle x y.$$$

Lean4

@[simp]
theorem sameCycle_subtypePerm {h} {x y : { x // p x }} : (f.subtypePerm h).SameCycle x y ↔ f.SameCycle x y :=
  exists_congr fun n => by simp [Subtype.ext_iff]

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