extendDomain — Mathlib

English

If g is a permutation-of α that is cycle-on s, and f is a map α → Subtype p, then the extension of g along f is a cycle-on f''s image.

Русский

Если g — перестановка на α, образующая цикл на s, и f — отображение α → Subtype p, то продолжение g вдоль f образует цикл на изображении f(s).

LaTeX

$$$\forall p, (g^{\mathrm{extendDomain} \; f}) \text{ IsCycleOn }( f''s ),$ где $f''s$ обозначает изображение $f$ из $s$.$$

Lean4

theorem extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (h : g.IsCycleOn s) :
    (g.extendDomain f).IsCycleOn ((↑) ∘ f '' s) :=
  ⟨h.1.extendDomain, by
    rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain⟩

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