extent_subset_extent_iff

Mathlib.Order.Concept

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

English

For any concepts c and d, c.extent is 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 \subseteq d.extent \iff c \le d$$$

Lean4

@[simp]
theorem extent_subset_extent_iff : c.extent ⊆ d.extent ↔ c ≤ d :=
  Iff.rfl

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

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

Разделы

Аффилиация

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