comp_eq_of_measurable_invariants — Mathlib

English

If g is measurable with respect to invariant f, then g ∘ f = g; i.e., g is invariant under f.

Русский

Если g измеримо относительно инвариантов f, то g ∘ f = g; то есть g инвариантна по отношению к f.

LaTeX

$$$$ g \\circ f = g $$$$

Lean4

theorem comp_eq_of_measurable_invariants {f : α → α} {g : α → β} [MeasurableSingletonClass β]
    (h : Measurable[invariants f] g) : g ∘ f = g := by
  funext x
  suffices x ∈ f ⁻¹' (g ⁻¹' {g x}) by simpa
  rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]

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