restrict_ofFunction — Mathlib

English

Under monotonic m, restrict s (ofFunction m) equals ofFunction with restricted m.

Русский

При монотонном m ограничение s от ofFunction равно ofFunction от m ограниченного на s.

LaTeX

$$$\\text{restrict\\_ofFunction }(s)(hm) = \\text{OuterMeasure.ofFunction } (\\lambda t. m (t \\cap s))\\ (by simp; simp [m\\_empty]).$$$

Lean4

theorem restrict_ofFunction (s : Set α) (hm : Monotone m) :
    restrict s (OuterMeasure.ofFunction m m_empty) =
      OuterMeasure.ofFunction (fun t => m (t ∩ s)) (by simp; simp [m_empty]) :=
  by
  rw [restrict]
  simp only [inter_comm _ s, LinearMap.comp_apply]
  rw [comap_ofFunction _ (Or.inl hm)]
  simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

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