isModularLattice_Ici

Mathlib.Order.ModularLattice

URI: https://scilib.ai/kg/mathlib#IsModularLattice.isModularLattice_Ici

← MathLib Explorer

English

The set Ici a inherits a modular lattice structure from the ambient lattice.

Русский

Множество Ici a наследует модульную структуру из исходной решётки.

LaTeX

$$$\text{IsModularLattice }(\mathrm{Set.Ici}\ a).Elem$$$

Lean4

instance isModularLattice_Ici : IsModularLattice (Set.Ici a) :=
  ⟨@fun x y z xz => (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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