lower

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#LowerSet.lower

English

The underlying set of a LowerSet is itself a lower set; i.e., the carrier of s is a lower set.

Русский

Базовое множество нижнего множества сами образует нижнее множество; то есть носитель s удовлетворяет свойству нижности.

LaTeX

$$IsLowerSet((s : Set α))$$

Lean4

@[simp]
protected theorem lower (s : LowerSet α) : IsLowerSet (s : Set α) :=
  s.lower'

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

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

Разделы

Аффилиация

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