tuple0_le — Mathlib

English

In the empty-index case Fin(0), any two functions f,g from Fin 0 to α i satisfy f ≤ g (pointwise).

Русский

В случае пустого индекса Fin(0) любые две функции f,g из Fin 0 в α i удовлетворяют f ≤ g (пойнт-в-диапазоне).

LaTeX

$$$\forall \ α,\ f,g: (i : Fin 0) \to α i,\ f \le g$$$

Lean4

theorem tuple0_le {α : Fin 0 → Type*} [∀ i, Preorder (α i)] (f g : ∀ i, α i) : f ≤ g :=
  finZeroElim

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