infsInfHom_apply

Mathlib.Order.Hom.CompleteLattice

URI: https://scilib.ai/kg/mathlib#infsInfHom_apply

English

The evaluation of infsInfHom on a pair gives the infimum.

Русский

Значение infsInfHom на паре даёт пересечение двух элементов.

LaTeX

$$$$ \mathrm{infsInfHom\_apply} : \mathrm{infsInfHom}(x) = x_1 \land x_2. $$$$

Lean4

@[simp, norm_cast]
theorem infsInfHom_apply : infsInfHom x = x.1 ⊓ x.2 :=
  rfl

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

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

Разделы

Аффилиация

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