isPiSystem_Iio

Mathlib.MeasureTheory.PiSystem

URI: https://scilib.ai/kg/mathlib#isPiSystem_Iio

English

IsPiSystem on the range of Iio: range Iio.

Русский

π-система на диапазоне Iio: range Iio.

LaTeX

$$$ IsPiSystem (range\ Iio) $$$

Lean4

theorem isPiSystem_Iio : IsPiSystem (range Iio : Set (Set α)) :=
  @image_univ α _ Iio ▸ isPiSystem_image_Iio univ

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

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

Разделы

Аффилиация

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