measurableSet_invariants — Mathlib

English

For a function f : α → α and g : α → β, g is measurable with respect to the invariant σ-algebra of f iff g is measurable and g^{-1}(s) = (g∘f)^{-1}(s) for every measurable set s.

Русский

Для функций f: α → α и g: α → β условие: Measurable[invariants f] g эквивалентно Measurable g и \\, g^{-1}(s) = (g∘f)^{-1}(s) для каждого измеримого s.

LaTeX

$$$Measurable[ invariants f ]\; g \\\\iff \\\\left(Measurable g \land \\\\\\forall s, \\, MeasurableSet s \\\\rightarrow (g \\\\circ f)^{-1} s = g^{-1} s\\\\right)$$$

Lean4

/-- A set `s` is `(invariants f)`-measurable
iff it is measurable w.r.t. the canonical σ-algebra on `α` and `f ⁻¹' s = s`. -/
theorem measurableSet_invariants {f : α → α} {s : Set α} :
    MeasurableSet[invariants f] s ↔ MeasurableSet s ∧ f ⁻¹' s = s :=
  .rfl

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