pair — Mathlib

English

Given elements a ≤ b in α, the map pair(a,b,hab) defines a Chain α by taking value a at index 0 and value b at all later indices; in particular, pair is monotone when hab holds.

Русский

Пусть a ≤ b в α. Определение pair(a, b, hab) задаёт цепь α так, что на индексе 0 стоит a, а на остальных индексах — b; цепь монотонна, если hab выполняется.

LaTeX

$$$$ \text{pair}(a,b,hab) : \text{Chain } \alpha, \quad (\text{pair}(a,b,hab))(0)=a, \quad (\text{pair}(a,b,hab))(n+1)=b, \quad a \le b. $$$$

Lean4

/-- An example of a `Chain` constructed from an ordered pair. -/
def pair (a b : α) (hab : a ≤ b) : Chain α
    where
  toFun
    | 0 => a
    | _ => b
  monotone' _ _ _ := by aesop

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