finMulAntidiag_one — Mathlib

English

For any d, finMulAntidiag d 1 equals the singleton set containing the constant-1 function.

Русский

Для любого d финальная антидиагональ равна одиночному множеству, содержащему единичную константную функцию.

LaTeX

$$$\text{finMulAntidiag}(d,1)=\{\text{const}_1:\, Fin d \to \mathbb{N}\}$$$

Lean4

theorem finMulAntidiag_one {d : ℕ} : finMulAntidiag d 1 = {fun _ => 1} :=
  by
  ext
  simp only [mem_finMulAntidiag, prod_eq_one_iff, mem_univ, forall_const, ne_eq, one_ne_zero, not_false_eq_true,
    and_true, mem_singleton]
  grind

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