iInter_true

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.iInter_true

English

If s is indexed by True, then the indexed intersection reduces to a single set: iInter s = s trivial.

Русский

Если индексы заданы True, пересечение сводится к единому множеству: iInter s = s trivial.

LaTeX

$$$ \mathrm{iInter}\; s = s\;\text{trivial}$$$

Lean4

@[simp]
theorem iInter_true {s : True → Set α} : iInter s = s trivial :=
  iInf_true

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

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

Разделы

Аффилиация

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