Iic_iInf

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.Iic_iInf

← MathLib Explorer

English

The principal lower set distributes over arbitrary infima: Iic(⨅ i, f i) = ⨅ i, Iic(f i).

Русский

Порожденное нижнее множество распределяется по обобщенным inf: Iic(⨅ i, f i) = ⨅ i, Iic(f i).

LaTeX

$$Iic (⨅ i, f i) = ⨅ i, Iic (f i)$$

Lean4

@[simp]
theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⨅ i, Iic (f i) :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf_iff, le_iInf_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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