sup_mem

Mathlib.Order.BooleanSubalgebra

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

English

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

Русский

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

LaTeX

$$$ a \in L \rightarrow b \in L \rightarrow a \lor b \in L $$$

Lean4

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

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

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

Разделы

Аффилиация

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