extent_ssubset_extent_iff

Mathlib.Order.Concept

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

English

For any concepts c and d, c.extent is strictly contained in d.extent if and only if c < d.

Русский

Для любых концептов c,d: c.extent строго входит в d.extent тогда и только тогда, когда c < d.

LaTeX

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

Lean4

@[simp]
theorem extent_ssubset_extent_iff : c.extent ⊂ d.extent ↔ c < d :=
  Iff.rfl

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

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

Разделы

Аффилиация

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