coe_inf

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#UpperSet.coe_inf

English

The underlying set of the infimum of two UpperSets is the union of their underlying sets.

Русский

Носитель пересечения двух верхних множеств равен объединению их носителей.

LaTeX

$$↑(s \sqcap t) = ↑s \cup ↑t$$

Lean4

@[simp, norm_cast]
theorem coe_inf (s t : UpperSet α) : (↑(s ⊓ t) : Set α) = (s : Set α) ∪ t :=
  rfl

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

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

Разделы

Аффилиация

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