inducedOuterMeasure_preimage — Mathlib

English

Final restatement aligning with iInf formulation for μ.

Русский

Окончательная формулировка через iInf для μ.

LaTeX

$$$\\mathrm{inducedOuterMeasure}\\ m P0 m0 s = iInf\\; (t) (ht) (s \\subseteq t)\\; m t ht$$$

Lean4

theorem inducedOuterMeasure_preimage (f : α ≃ α) (Pm : ∀ s : Set α, P (f ⁻¹' s) ↔ P s)
    (mm : ∀ (s : Set α) (hs : P s), m (f ⁻¹' s) ((Pm _).mpr hs) = m s hs) {A : Set α} :
    inducedOuterMeasure m P0 m0 (f ⁻¹' A) = inducedOuterMeasure m P0 m0 A :=
  by
  rw [inducedOuterMeasure_eq_iInf _ msU m_mono, inducedOuterMeasure_eq_iInf _ msU m_mono]; symm
  refine f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_
  refine iInf_congr_Prop (Pm s) ?_; intro hs
  refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_
  intro _; exact mm s hs

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