card_mul_eq_card_mul — Mathlib

English

Equality of the two products in the double counting set-up: |s|·m = |t|·n when both sides attain exact bounds.

Русский

Равенство двух произведений в конфигурации двойного подсчета: |s|·m = |t|·n при достижении точных границ.

LaTeX

$$$$ |s| \cdot m = |t| \cdot n $$$$

Lean4

theorem card_mul_eq_card_mul [∀ a b, Decidable (r a b)] (hm : ∀ a ∈ s, #(t.bipartiteAbove r a) = m)
    (hn : ∀ b ∈ t, #(s.bipartiteBelow r b) = n) : #s * m = #t * n :=
  (card_mul_le_card_mul _ (fun a ha ↦ (hm a ha).ge) fun b hb ↦ (hn b hb).le).antisymm <|
    card_mul_le_card_mul' _ (fun a ha ↦ (hn a ha).ge) fun b hb ↦ (hm b hb).le

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