left

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GCongr.AntisymmRel.left

English

From AntisymmRel r a b one can read off the left component, namely r a b.

Русский

Из AntisymmRel r a b следует левая компонента: r a b.

LaTeX

$$$\text{AntisymmRel}(r)\,a\,b \to r\,a\,b$$$

Lean4

theorem left (h : AntisymmRel r a b) : r a b :=
  h.1

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

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

Разделы

Аффилиация

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