inf_mem

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.inf_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 inf_mem (ha : a ∈ L) (hb : b ∈ L) : a ⊓ b ∈ L :=
  L.infClosed ha hb

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

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

Разделы

Аффилиация

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