lambda — Mathlib

English

The lambda function of the incidence algebra is the function that assigns 1 to every nonempty interval of cardinality one or two; otherwise 0.

Русский

Функция λ инцидентной алгебры принимает значение 1 на любом непустом интервале размером 1 или 2 и 0 в остальных случаях.

LaTeX

$$$$ \\lambda(a,b) = \\begin{cases} 1, & a=b \\text{ or } a \\lessdot b, \\\\ 0, & \\text{otherwise}. \\end{cases} $$$$

Lean4

/-- The lambda function of the incidence algebra is the function that assigns `1` to every nonempty
interval of cardinality one or two. -/
@[simps]
def lambda : IncidenceAlgebra 𝕜 α :=
  ⟨fun a b ↦ if a ⩿ b then 1 else 0, fun _a _b h ↦ if_neg fun hh ↦ h hh.le⟩

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