two_mul_card_image_offDiag — Mathlib

English

The off-diagonal pairs contribute exactly half of the total two-element image: 2 times the size of the image equals the off-diagonal cardinal.

Русский

Без диагонали пары вносит точно половину общего изображения двух элементов: 2×|image| = |offDiag|.

LaTeX

$$$2 \cdot |(s.offDiag).image(\mathrm{Sym2.mk})| = |s.offDiag|$$$

Lean4

theorem two_mul_card_image_offDiag (s : Finset α) : 2 * #(s.offDiag.image Sym2.mk) = #s.offDiag :=
  by
  rw [card_eq_sum_card_image (Sym2.mk : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]
  rintro x y hxy
  simp_rw [mem_image, mem_offDiag] at hxy
  obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy
  replace h := Sym2.eq.1 h
  obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by cases h <;> refine ⟨‹_›, ‹_›, ?_⟩ <;> [exact ha; exact ha.symm]
  have hxy' : y ≠ x := hxy.symm
  have : {z ∈ s.offDiag | Sym2.mk z = s(x, y)} = {(x, y), (y, x)} :=
    by
    ext ⟨x₁, y₁⟩
    rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk_inj, Prod.mk_inj, and_iff_right_iff_imp]
      -- `hxy'` is used in `exact`

    rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩
  rw [this, card_insert_of_notMem, card_singleton]
  simp only [not_and, Prod.mk_inj, mem_singleton]
  exact fun _ => hxy'

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