le

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.le

English

If a is covered by b in the WCovBy sense, then a ≤ b.

Русский

Если a покрывает b в смысле WCovBy, то a ≤ b.

LaTeX

$$$\\\\forall a,b,\\\\, h: a \\\\mathrel{\\\\trianglelefteq} b \\\\Rightarrow a \\\\le b.$$$

Lean4

theorem le (h : a ⩿ b) : a ≤ b :=
  h.1

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

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

Разделы

Аффилиация

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