isPiSystem_Iic

Mathlib.MeasureTheory.PiSystem

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

English

The family { (−∞, a] : a ∈ α } (the range of Iic) is a π-system.

Русский

Семейство { (−∞, a] : a ∈ α } (диапазон Iic) образует π-систему.

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ Iic(a) : a \in \alpha \}\right) $$$$

Lean4

theorem isPiSystem_Iic : IsPiSystem (range Iic : Set (Set α)) :=
  @image_univ α _ Iic ▸ isPiSystem_image_Iic univ

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

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

Разделы

Аффилиация

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