intent_inf

Mathlib.Order.Concept

URI: https://scilib.ai/kg/mathlib#Concept.intent_inf

English

The meet’s intent is the upper polar of the intersection of extents.

Русский

Интенция пересечения равна верхней полярной от пересечения экстентов.

LaTeX

$$$(c \inf d).intent = \operatorname{upperPolar}_r( c.extent \cap d.extent )$$$

Lean4

@[simp]
theorem intent_inf (c d : Concept α β r) : (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent) :=
  rfl

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

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

Разделы

Аффилиация

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