ヤングアニマル Web に数学ゴールデンがあった (https://younganimal.com/series/a2c408d4be5da/) ので読んだら鳩の巣原理が出てきて、証明できそうだったのでやってみた。有限集合の濃度の不等号を仮定に単射が存在しないことを示す方針、本質は単射から濃度の不等号を導く部分っぽい (A.card ≤ B.card を証明する部分)。Classical.choice が混ざってしまっている。

import Mathlib.Data.Finset.Card

open Finset

theorem pigeonhole { α : Type u } { β : Type v } [DecidableEq β]:
  ∀ (A : Finset α) (B : Finset β), A.card > B.card → ¬ (∃ (f : α → β), A.image f ⊆ B ∧ Set.InjOn f A) :=
  fun A B h_card_gt h_exists =>
    have h_card_le : A.card ≤ B.card := h_exists.elim
      fun f h_inj =>
        calc A.card
          _ = (A.image f).card := Eq.symm (card_image_of_injOn h_inj.right)
          _ ≤ B.card           := card_le_of_subset h_inj.left
    absurd h_card_le (by simp [h_card_gt])

/-
'pigeonhole' depends on axioms: [propext, Quot.sound, Classical.choice]
-/
#print axioms pigeonhole

感想

最初関数を f : A -> B と書こうとしたが、それでは像 A.image f の型が合わなかった
証明済みの定理を探すのが辛く Mathlib.Tactic.LibrarySearch もあまり助けてくれない
次はプログラミング的な側面を実験していきたい、日付型とかで面白い証明考えられないだろうか
DecidableEq は当然わかっていない、わからないことが多い
ヤングアニマル Web は読み込み遅い？

ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

Lean4 学習7

感想