isCountablySpanning

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

English

If μ has finite spanning sets in C, then C is countably spanning.

Русский

Если μ имеет конечные охватывающие множества в C, то C является счётно охватывающим.

LaTeX

$$$(h : μ.FiniteSpanningSetsIn C) : IsCountablySpanning C$$$

Lean4

protected theorem isCountablySpanning (h : μ.FiniteSpanningSetsIn C) : IsCountablySpanning C :=
  ⟨h.set, h.set_mem, h.spanning⟩

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

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

Разделы

Аффилиация

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