le

Mathlib.ModelTheory.Order

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Term.le

← MathLib Explorer

English

Joins two terms in a formula representing t1 ≤ t2.

Русский

Объединение двух термов в формуле, представляющее t1 ≤ t2.

LaTeX

$$$ t_1.le t_2 $$$

Lean4

/-- Joins two terms `t₁, t₂` in a formula representing `t₁ ≤ t₂`. -/
def le (t₁ t₂ : L.Term (α ⊕ (Fin n))) : L.BoundedFormula α n :=
  leSymb.boundedFormula₂ t₁ t₂

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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