edge₃ — Mathlib

English

An alternative edge constructor for Λ[n,i] when n ≥ 3, built from the basic edge with a cardinality bound.

Русский

Альтернативный конструктор ребра для Λ[n,i] при n ≥ 3, получаемый из базового ребра с ограничением кардинальности.

LaTeX

$$$\mathrm{edge}_3(n,i,a,b,hab,H) : (\Lambda[n,i]).(1) $$$

Lean4

/-- Alternative constructor for the edge of `Λ[n, i]` with endpoints `a` and `b`,
assuming `3 ≤ n`. -/
@[simps!]
def edge₃ (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n) : (Λ[n, i] : SSet.{u}) _⦋1⦌ :=
  edge n i a b hab <| Finset.card_le_three.trans H

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