coe_inf

Mathlib.Algebra.Ring.Subsemiring.Defs

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

English

The infimum of subsemirings corresponds to intersection of carriers.

Русский

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

LaTeX

$$$((p \sqcap p' : \mathrm{Subsemiring}(R)) : Set R) = (p : Set R) \cap p'$$$

Lean4

@[simp, norm_cast]
theorem coe_inf (p p' : Subsemiring R) : ((p ⊓ p' : Subsemiring R) : Set R) = (p : Set R) ∩ p' :=
  rfl

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

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

Разделы

Аффилиация

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