coe_inf'

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.coe_inf'

English

The carrier of the infimum of two Sublattices equals the intersection of their carriers.

Русский

Носитель наименьшей подрешётки равен пересечению носителей двух подрешёток.

LaTeX

$$$(L \sqcap M : \text{Sublattice } \alpha) = (L : \mathrm{Set} \alpha) \cap M$$$

Lean4

@[simp, norm_cast]
theorem coe_inf' (L M : Sublattice α) : L ⊓ M = (L : Set α) ∩ M :=
  rfl

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

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

Разделы

Аффилиация

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