inducedOuterMeasure_eq_iInf — Mathlib

English

Extend preserves monotonicity with P on s1, s2 and s1 ⊆ s2; extend m s1 ≤ extend m s2.

Русский

Расширение сохраняет монотонность при s1 ⊆ s2 и P на s1: extend m s1 ≤ extend m s2.

LaTeX

$$$P s_1 \\land s_1 \\subseteq s_2 \\Rightarrow \\mathrm{extend}\\ m\\ s_1 \\le \\mathrm{extend}\\ m\\ s_2$$$

Lean4

theorem inducedOuterMeasure_eq_iInf (s : Set α) :
    inducedOuterMeasure m P0 m0 s = ⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht :=
  by
  apply le_antisymm
  · simp only [le_iInf_iff]
    intro t ht hs
    grw [hs]
    exact le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)
  · refine le_iInf ?_
    intro f
    refine le_iInf ?_
    intro hf
    refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)
    refine le_iInf ?_
    intro h2f
    exact iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)

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