MeasurableSpace.measurableSet_invariants

theorem MeasurableSpace.measurableSet_invariants : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α}, MeasurableSet s ↔ MeasurableSet s ∧ f ⁻¹' s = s

The theorem `MeasurableSpace.measurableSet_invariants` states that, for any type `α`, any `MeasurableSpace` instance on it, any function `f` from `α` to `α`, and any set `s` of type `α`, the set `s` is `(invariants f)`-measurable if and only if it is measurable with respect to the canonical sigma-algebra on `α` and that the preimage of `s` under `f` is equal to `s`. In simple terms, it states that a set is measurable under certain conditions if it is measurable according to a given measure and it remains unchanged when you apply the function `f` and then reverse that application.

More concisely: A set is `(invariants f)`-measurable if and only if it is measurable and its preimage under `f` is equal to the set itself.