isPiSystem_image_Ici

Mathlib.MeasureTheory.PiSystem

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

English

For a subset s of α, the family { Ici(a) : a ∈ s } is a π-system, where Ici(a) = [a, ∞).

Русский

Для подмножества s ⊆ α семейство { [a, ∞) : a ∈ s } образует π-систему, где Ici(a) = [a, ∞).

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ Ici(a) : a \in s \}\right) $$$$

Lean4

theorem isPiSystem_image_Ici (s : Set α) : IsPiSystem (Ici '' s) :=
  @isPiSystem_image_Iic αᵒᵈ _ s

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

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

Разделы

Аффилиация

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