univLE_of_max

Mathlib.Logic.UnivLE

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

English

From UnivLE at (max u v, v) we obtain UnivLE(u, v) via transitivity; order does not matter.

Русский

Из UnivLE на (max u v, v) следует UnivLE(u, v) через транзитивность; порядок не имеет значения.

LaTeX

$$$\mathrm{UnivLE}(u,v)$$$

Lean4

instance univLE_of_max [UnivLE.{max u v, v}] : UnivLE.{u, v} :=
  @UnivLE.trans univLE_max
    ‹_›
      -- order doesn't matter

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

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

Разделы

Аффилиация

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