coe_inf

Mathlib.RingTheory.NonUnitalSubring.Basic

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

English

The underlying set of the infimum of p and p′ is p ∩ p′.

Русский

Множество нижнего предела p ⊓ p′ равно пересечению p и p′ по множествам.

LaTeX

$$$(p \\inf p') : Set R = p \\cap p'$$$

Lean4

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

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

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

Разделы

Аффилиация

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