innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group

English

InnerRegularWRT μ with respect to sets that are compact and closed, using MeasurableSet and finiteness of μ.

Русский

Внутренняя регулярность по множестваcм, которые компактны и замкнуты, для меры μ с условием измеримости и конечности μ.

LaTeX

$$$\text{InnerRegularWRT}\,\mu\, (\lambda s. \text{IsCompact}(s) \wedge \text{IsClosed}(s))\, (\lambda s. \text{MeasurableSet}(s) \wedge \mu(s) \neq \infty)$$$

Lean4

@[to_additive]
theorem innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [h : InnerRegularCompactLTTop μ] :
    InnerRegularWRT μ (fun s ↦ IsCompact s ∧ IsClosed s) (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) :=
  by
  intro s ⟨s_meas, μs⟩ r hr
  rcases h.innerRegular ⟨s_meas, μs⟩ r hr with ⟨K, Ks, K_comp, hK⟩
  refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
  · exact IsCompact.closure_subset_measurableSet K_comp s_meas Ks
  · rwa [K_comp.measure_closure]

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