strictAnti_intent

Mathlib.Order.Concept

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

English

Intent is strictly anti-monotone: if c < d then d.intent ⊂ c.intent.

Русский

Интенция строго антимонотонна: если c < d, то d.intent ⊂ c.intent.

LaTeX

$$$\forall c,d : \mathrm{Concept}\,\alpha\,\beta\,r,\; c < d \rightarrow d.intent \subset c.intent$$$

Lean4

theorem strictAnti_intent : StrictAnti (@intent α β r) := fun _ _ => intent_ssubset_intent_iff.2

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

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

Разделы

Аффилиация

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