antidiagonal_single — Mathlib

English

The antidiagonal of a single element is obtained by mapping through a product map of single-valued injections.

Русский

Антидиагональ единичного элемента получается путем отображения через отображение произведения инъекций.

LaTeX

$$∀ a, n,\\; \\operatorname{antidiagonal}(\\mathrm{single}\\ a\\ n) = \\mathrm{Finset.map}( \\{ toFun := \\mathrm{single}\\ a, inj' := \\mathrm{single\\_injective}\\ a \\} .prodMap { toFun := \\mathrm{single}\\ a, inj' := \\mathrm{single\\_injective}\\ a }) (\\mathrm{Finset.Nat.instHasAntidiagonal}.antidiagonal n)$$

Lean4

@[simp]
theorem antidiagonal_single (a : α) (n : ℕ) :
    antidiagonal (single a n) =
      (antidiagonal n).map (Function.Embedding.prodMap ⟨_, single_injective a⟩ ⟨_, single_injective a⟩) :=
  by
  ext ⟨x, y⟩
  simp only [mem_antidiagonal, mem_map, mem_antidiagonal, Function.Embedding.coe_prodMap, Function.Embedding.coeFn_mk,
    Prod.map_apply, Prod.mk.injEq, Prod.exists]
  constructor
  · intro h
    refine ⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
    simp_rw [DFunLike.ext_iff, ← forall_and]
    intro i
    replace h := DFunLike.congr_fun h i
    simp_rw [single_apply, Finsupp.add_apply] at h ⊢
    obtain rfl | hai := Decidable.eq_or_ne a i
    · exact ⟨if_pos rfl, if_pos rfl⟩
    · simp_rw [if_neg hai, add_eq_zero] at h ⊢
      exact h.imp Eq.symm Eq.symm
  · rintro ⟨a, b, rfl, rfl, rfl⟩
    exact (single_add _ _ _).symm

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