everywherePosSubset_subset

Mathlib.MeasureTheory.Measure.EverywherePos

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

English

EverywherePosSubset of s is contained in s.

Русский

Подмножество everywherePosSubset(S) содержится в S.

LaTeX

$$$$ μ.everywherePosSubset s \\subseteq s. $$$$

Lean4

theorem everywherePosSubset_subset (μ : Measure α) (s : Set α) : μ.everywherePosSubset s ⊆ s := fun _x hx ↦ hx.1

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

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

Разделы

Аффилиация

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