sup_mem

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.sup_mem

English

If a,b ∈ L then a ⊔ b ∈ L.

Русский

Если a,b ∈ L, то a ⊔ b ∈ L.

LaTeX

$$ (ha : a ∈ L) (hb : b ∈ L) : a ⊔ b ∈ L$$

Lean4

theorem sup_mem (ha : a ∈ L) (hb : b ∈ L) : a ⊔ b ∈ L :=
  L.supClosed ha hb

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

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

Разделы

Аффилиация

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