IsComplemented

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#IsComplemented

English

An element a is complemented if there exists b with IsCompl a b.

Русский

Элемент a комплементирован, если существует b такое, что IsCompl a b.

LaTeX

$$$IsComplemented(a) \\equiv \\exists b, IsCompl(a,b)$$$

Lean4

/-- An element is *complemented* if it has a complement. -/
def IsComplemented (a : α) : Prop :=
  ∃ b, IsCompl a b

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

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

Разделы

Аффилиация

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