measurable_invariants_of_semiconj

English

If g is measurable and g semiconjugates fa to fb, then g is measurable between the invariant spaces: invariants fa to invariants fb.

Русский

Если g измеримо и является полусопряжением g fa → fb, то g измеримо между инвариантными пространствами: invariants fa ⟶ invariants fb.

LaTeX

$$$\\\\forall fa fb g \\\\ (hg : Measurable g) \\\\ (hfg : Semiconj g fa fb), \\\\ Measurable[ invariants fa ] ( invariants fb ) g$$$

Lean4

theorem measurable_invariants_of_semiconj {fa : α → α} {fb : β → β} {g : α → β} (hg : Measurable g)
    (hfg : Semiconj g fa fb) : @Measurable _ _ (invariants fa) (invariants fb) g := fun s hs ↦
  ⟨hg hs.1, by rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]⟩

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