isLowerSet_setOf

Mathlib.Order.UpperLower.Basic

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

English

The set {a | p(a)} is a lower set iff p is antitone.

Русский

Множество {a | p(a)} является нижним множеством тогда и только тогда, когда p антитонична.

LaTeX

$$$\operatorname{IsLowerSet}(\{a \mid p(a)\}) \iff \operatorname{Antitone}(p)$$$

Lean4

@[simp]
theorem isLowerSet_setOf : IsLowerSet {a | p a} ↔ Antitone p :=
  forall_swap

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

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

Разделы

Аффилиация

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