of_imp

Mathlib.MeasureTheory.Measure.Regular

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.InnerRegularWRT.of_imp

English

If q implies p for every set, then μ is inner regular with respect to p and q.

Русский

Если для каждого множества верно q(s) ⇒ p(s), то μ обладает внутренней регулярностью по p,q.

LaTeX

$$$(\forall s, q(s) \to p(s)) \Rightarrow InnerRegularWRT(\mu; p, q).$$$

Lean4

theorem of_imp (h : ∀ s, q s → p s) : InnerRegularWRT μ p q := fun U hU _ hr ↦ ⟨U, Subset.rfl, h U hU, hr⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru