measurable_invariants_dom — Mathlib

English

Let f : α → α and g : α → β. Then g is measurable with respect to invariants f iff g is measurable and ∀ s, MeasurableSet s → (g ∘ f)^{-1} s = g^{-1} s.

Русский

Пусть f: α → α и g: α → β. Тогда g измеримо относительно инвариантов f тогда и только тогда, когда g измеримо и для любого измеримого множества s выполняется (g ∘ f)^{-1} s = g^{-1} 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

theorem measurable_invariants_dom {f : α → α} {g : α → β} :
    Measurable[invariants f] g ↔ Measurable g ∧ ∀ s, MeasurableSet s → (g ∘ f) ⁻¹' s = g ⁻¹' s := by
  simp only [Measurable, ← forall_and]; rfl

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