const_inf

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.const_inf

English

The embedding β → Germ l β preserves infimum: the germ of a⊓b equals the infimum of the germs of a and b.

Русский

Встраивание β в Germ l β сохраняет инфимум: germ(a ⊓ b) = germ(a) ⊓ germ(b).

LaTeX

$$$\\mathrm{Germ.const}(a \\;⊓\\; b) = (\\mathrm{Germ.const}(a) \\;⊓\\; \\mathrm{Germ.const}(b))$$$

Lean4

@[simp, norm_cast]
theorem const_inf [Min β] (a b : β) : ↑(a ⊓ b) = (↑a ⊓ ↑b : Germ l β) :=
  rfl

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

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

Разделы

Аффилиация

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