supsSupHom_apply

Mathlib.Order.Hom.CompleteLattice

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

English

The evaluation of supsSupHom on a pair gives the join.

Русский

Значение supsSupHom на паре даёт объединение двух элементов.

LaTeX

$$$$ \mathrm{supsSupHom\_apply} : \mathrm{supsSupHom}(x) = x_1 \lor x_2. $$$$

Lean4

@[simp, norm_cast]
theorem supsSupHom_apply : supsSupHom x = x.1 ⊔ x.2 :=
  rfl

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

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

Разделы

Аффилиация

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