sInf_apply

Mathlib.Order.Nucleus

URI: https://scilib.ai/kg/mathlib#Nucleus.sInf_apply

English

The sInf operation applied to a set of nuclei yields a nucleus whose action is the infimum of the actions on each input.

Русский

Операция sInf над множеством нуклеусов даёт нуклеус с инфимум-действием на каждом входе.

LaTeX

$$$sInf\,s\;x = \bigwedge_{j\in s} j(x)$$$

Lean4

@[simp]
theorem sInf_apply (s : Set (Nucleus X)) (x : X) : sInf s x = ⨅ j ∈ s, j x :=
  rfl

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

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

Разделы

Аффилиация

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