coe_inf

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.coe_inf

English

The underlying set of p ⊓ q equals p ∩ q.

Русский

Подмодульное множество p ⊓ q совпадает с множеством p ∩ q.

LaTeX

$$$\uparrow(p \cap q) = \uparrow p \cap \uparrow q$$$

Lean4

@[simp]
theorem coe_inf : ↑(p ⊓ q) = (p ∩ q : Set M) :=
  rfl

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

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

Разделы

Аффилиация

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