English
There are (card β)^(card α) functions from α to β; i.e., |α → β| = |β|^{|α|}.
Русский
Матов существует (|β|)^{|α|} функций из α в β; то есть |α → β| = |β|^{|α|}.
LaTeX
$$$$ \\left|\\alpha \\to \\beta\\right| = \\left|\\beta\\right|^{\\left|\\alpha\\right|}. $$$$
Lean4
@[simp]
theorem card_fun {α β : Type*} : card (α → β) = (card β) ^ card α := by
classical
rcases isEmpty_or_nonempty α with α_emp | α_emp
· simp [(card_eq_zero_iff_empty α).2 α_emp]
rcases finite_or_infinite α
· rcases finite_or_infinite β
· letI := Fintype.ofFinite α
letI := Fintype.ofFinite β
simp
· simp only [card_eq_top_of_infinite]
exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
· rw [card_eq_top_of_infinite (α := α)]
rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
· rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
simp [b_0]
· rw [b_1, one_epow]
apply le_antisymm
· letI := (card_le_one_iff_subsingleton β).1 b_1.le
exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
· letI := (one_le_card_iff_nonempty β).1 b_1.ge
exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
· rw [epow_top b_2, card_eq_top]
rw [one_lt_card_iff_nontrivial β] at b_2
exact Pi.infinite_of_left
