Compatibility of the invariant σ-algebras with the Borel structure (issue #28, commit 2)

The invariant σ-algebras of InvariantMeasurableSpace.lean sit below the ambient product (Borel) σ-algebra, and the model classes ModelsOf φ are measurable in them.

• MeasurableSpace.smulInvariant_le (and the named actionInvariantMeasurableSpace_le, isoInvariantMeasurableSpace_le): the invariant σ-algebra is coarser than the base one, so the identity X → X from the base space to the invariant space is measurable (measurable_id_smulInvariant and the named forms) — the correct direction.
• measurableSet_isoInvariant_modelsOf / measurableSet_actionInvariant_modelsOf: ModelsOf φ is measurable in either named invariant σ-algebra, under exactly the hypotheses of the existing satisfaction-measurability theorem modelsOf_measurableSet (relational vocabulary only — no countability, no Polishness).
• MeasurableSet.of_actionInvariant / MeasurableSet.of_isoInvariant and measurableSet_actionInvariant_iff_isoInvariant: convenience lemmas for consuming these statements without temporarily installing a global MeasurableSpace instance.

theorem MeasurableSpace.smulInvariant_le {G : Type u_1} {X : Type u_2} [SMul G X] (m : MeasurableSpace X) : smulInvariant G m ≤ m

The generic invariant σ-algebra is coarser than its base.

theorem MeasurableSpace.measurable_id_smulInvariant {G : Type u_1} {X : Type u_2} [SMul G X] (m : MeasurableSpace X) : Measurable id

The identity from the base space to the (coarser) invariant σ-algebra is measurable.

Coarseness and the identity map

theorem FirstOrder.Language.actionInvariantMeasurableSpace_le {L : Language} : actionInvariantMeasurableSpace ≤ instMeasurableSpaceStructureSpace

actionInvariantMeasurableSpace is coarser than the ambient product σ-algebra.

theorem FirstOrder.Language.isoInvariantMeasurableSpace_le {L : Language} [L.IsRelational] : isoInvariantMeasurableSpace ≤ instMeasurableSpaceStructureSpace

isoInvariantMeasurableSpace is coarser than the ambient product σ-algebra.

theorem FirstOrder.Language.measurable_id_actionInvariant {L : Language} : Measurable id

The identity from the ambient Borel space to actionInvariantMeasurableSpace is measurable.

theorem FirstOrder.Language.measurable_id_isoInvariant {L : Language} [L.IsRelational] : Measurable id

The identity from the ambient Borel space to isoInvariantMeasurableSpace is measurable.

Consuming invariant-measurability

theorem FirstOrder.Language.MeasurableSet.of_actionInvariant {L : Language} {B : Set L.StructureSpace} (h : MeasurableSet B) : MeasurableSet B

An action-invariant-measurable class is measurable in the ambient Borel space.

theorem FirstOrder.Language.MeasurableSet.of_isoInvariant {L : Language} [L.IsRelational] {B : Set L.StructureSpace} (h : MeasurableSet B) : MeasurableSet B

An isomorphism-invariant-measurable class is measurable in the ambient Borel space.

theorem FirstOrder.Language.measurableSet_actionInvariant_iff_isoInvariant {L : Language} [L.IsRelational] {B : Set L.StructureSpace} : MeasurableSet B ↔ MeasurableSet B

The two invariant σ-algebras have the same measurable sets — a convenient bridge for consuming either statement without installing a global instance.

Model classes are invariant-measurable

theorem FirstOrder.Language.measurableSet_isoInvariant_modelsOf {L : Language} [L.IsRelational] (φ : L.Sentenceω) : MeasurableSet (ModelsOf φ)

ModelsOf φ is isomorphism-invariant-measurable — under exactly the hypothesis of the satisfaction-measurability theorem (relational vocabulary; no countability, no Polishness).

theorem FirstOrder.Language.measurableSet_actionInvariant_modelsOf {L : Language} [L.IsRelational] (φ : L.Sentenceω) : MeasurableSet (ModelsOf φ)

ModelsOf φ is action-invariant-measurable — same hypothesis.